mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case a
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
hph : p ^ Nat.find ⋯ ≠ 0
⊢ p.count a.factors ≤ Nat.find ⋯

Tactic:
rcases subsingleton_or_nontrivial α with hα | hα

Goal state after:
case a.inl
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
hph : p ^ Nat.find ⋯ ≠ 0
hα : Subsingleton α
⊢ p.count a.factors ≤ Nat.find ⋯

case a.inr
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
hph : p ^ Nat.find ⋯ ≠ 0
hα : Nontrivial α
⊢ p.count a.factors ≤ Nat.find ⋯
Module: Mathlib.Algebra.Central.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
this : IsCentral K D
x : K
⊢ ∃ a, (algebraMap k K) a = x

Tactic:
have H : algebraMap K D x ∈ (Subalgebra.center K D : Set D) := Subalgebra.algebraMap_mem _ _

Goal state after:
k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
this : IsCentral K D
x : K
H : (algebraMap K D) x ∈ ↑(Subalgebra.center K D)
⊢ ∃ a, (algebraMap k K) a = x
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case add
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
x y : Q ⊗[R] P
hx : ∃ a, (lTensor Q g) a = x
hy : ∃ a, (lTensor Q g) a = y
⊢ ∃ a, (lTensor Q g) a = x + y

Tactic:
obtain ⟨x, rfl⟩ := hx

Goal state after:
case add
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
y : Q ⊗[R] P
hy : ∃ a, (lTensor Q g) a = y
x : Q ⊗[R] N
⊢ ∃ a, (lTensor Q g) a = (lTensor Q g) x + y
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case add
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
x y : P ⊗[R] Q
hx : ∃ a, (rTensor Q g) a = x
hy : ∃ a, (rTensor Q g) a = y
⊢ ∃ a, (rTensor Q g) a = x + y

Tactic:
obtain ⟨x, rfl⟩ := hx

Goal state after:
case add
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
y : P ⊗[R] Q
hy : ∃ a, (rTensor Q g) a = y
x : N ⊗[R] Q
⊢ ∃ a, (rTensor Q g) a = (rTensor Q g) x + y
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : CharZero R
x y : ℕ
hxy : ↑x = ↑y
⊢ x = y

Tactic:
rwa [← C_eq_coe_nat, ← C_eq_coe_nat, C_inj, Nat.cast_inj] at hxy

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.refine_4.tmul.tmul
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
a : A
b : B
x : ↥(Submodule.restrictScalars R I)
y : B
⊢ ∃ y_1,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (x ⊗ₜ[R] y)

Tactic:
use (a • x) ⊗ₜ[R] (b * y)

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
a : A
b : B
x : ↥(Submodule.restrictScalars R I)
y : B
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) ((a • x) ⊗ₜ[R] (b * y)) =
    a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (x ⊗ₜ[R] y)
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
⊢ Submodule.restrictScalars R (map includeLeft I) = (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype).range

Tactic:
by
  rw [← SetLike.coe_set_eq]
  apply le_antisymm
  · intro x hx
    simp only [SetLike.mem_coe, LinearMap.mem_range]
    rw [Ideal.map, ← submodule_span_eq] at hx
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hx
    · intro x
      simp only [includeLeft_apply, Set.mem_image, SetLike.mem_coe]
      rintro ⟨y, hy, rfl⟩
      use ⟨y, hy⟩ ⊗ₜ[R] 1
      rfl
    · use 0
      simp only [map_zero]
    · rintro x y - - ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
      use x + y
      simp only [map_add]
    · rintro a x - ⟨x, hx, rfl⟩
      induction a with
      | zero =>
        use 0
        simp only [map_zero, smul_eq_mul, zero_mul]
      | tmul a b =>
        induction x with
        | zero =>
          use 0
          simp only [map_zero, smul_eq_mul, mul_zero]
        | tmul x y =>
          use (a • x) ⊗ₜ[R] (b * y)
          simp only [smul_eq_mul]
          with_unfolding_all rfl
        | add x y hx hy =>
          obtain ⟨x', hx'⟩ := hx
          obtain ⟨y', hy'⟩ := hy
          use x' + y'
          simp only [map_add, hx', smul_add, hy']
      | add a b ha hb =>
        obtain ⟨x', ha'⟩ := ha
        obtain ⟨y', hb'⟩ := hb
        use x' + y'
        simp only [map_add, ha', add_smul, hb']
  · rintro x ⟨y, rfl⟩
    induction y with
    | zero =>
        rw [map_zero]
        apply zero_mem
    | tmul a b =>
        simp only [LinearMap.rTensor_tmul, Submodule.coe_subtype]
        suffices (a : A) ⊗ₜ[R] b = ((1 : A) ⊗ₜ[R] b) * ((a : A) ⊗ₜ[R] (1 : B)) by
          simp only [Submodule.coe_restrictScalars, SetLike.mem_coe]
          rw [this]
          apply Ideal.mul_mem_left
          -- Note: adding `includeLeft` as a hint fixes a timeout https://github.com/leanprover-community/mathlib4/pull/8386
          apply Ideal.mem_map_of_mem includeLeft
          exact Submodule.coe_mem a
        simp only [Algebra.TensorProduct.tmul_mul_tmul,
          mul_one, one_mul]
    | add x y hx hy =>
        rw [map_add]
        apply Submodule.add_mem _ hx hy

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
⊢ ∃ M' N',
    ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(map (inclusion hM) (inclusion hN)).range

Tactic:
obtain ⟨M', N', _, _, h⟩ := exists_finite_submodule_of_setFinite s hs
  have hM := map_subtype_le M₁ M'
  have hN := map_subtype_le N₁ N'
  refine ⟨_, _, hM, hN, .map _ _, .map _ _, ?_⟩
  rw [mapIncl,
    show M'.subtype = inclusion hM ∘ₗ M₁.subtype.submoduleMap M' by ext; simp,
    show N'.subtype = inclusion hN ∘ₗ N₁.subtype.submoduleMap N' by ext; simp,
    map_comp] at h
  exact h.trans (LinearMap.range_comp_le_range _ _)

Goal state after:
Module: Mathlib.Algebra.Azumaya.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x✝ : (n × n) × n × n
i0 j0 k0 l0 : n
⊢ (mulLeftRightMatrix_inv R n ∘ₗ (mulLeftRight R (Matrix n n R)).toLinearMap)
      (((stdBasis R n n).tensorProduct ((stdBasis R n n).map (opLinearEquiv R))) ((i0, j0), k0, l0)) =
    LinearMap.id (((stdBasis R n n).tensorProduct ((stdBasis R n n).map (opLinearEquiv R))) ((i0, j0), k0, l0))

Tactic:
by
    simp [stdBasis_eq_single, ite_and, Fintype.sum_prod_type,
      mulLeftRight_apply, single, Matrix.mul_apply]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj₁ : 0 < j
hj₂ : j - 1 < k
⊢ (F.intervalGapsWithin h a b ↑j).1 = ((F.orderEmbOfFin h) ⟨j - 1, hj₂⟩).2

Tactic:
by
  convert! F.intervalGapsWithin_succ_fst_of_lt h a b (j - 1) hj₂
  omega

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
t : Finset κ
f : ι × κ → M
⊢ 𝔼 x ∈ s ×ˢ t, f x = 𝔼 i ∈ s, 𝔼 j ∈ t, f (i, j)

Tactic:
simp only [expect, card_product, sum_product, smul_sum, mul_inv, mul_smul, Nat.cast_mul]

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → DivisionRing (G i)
inst✝² : DivisionRing C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
q : ℚ
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝²
⊢ (f x✝² x✝¹ x✝) (q • x) = q • (f x✝² x✝¹ x✝) x

Tactic:
by
    simp_rw [Rat.smul_def, map_mul, map_ratCast]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: case hi
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a ∈ range k, ((p ↑a).2, (p ↑a.succ).1) ∈ F

Tactic:
exact fun i _ ↦ F.intervalGapsWithin_mapsTo h a b (x := i) (by grind)

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inl.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
Int.add_mul_emod_self_left,

Goal state after:
case inr.mpr.inl.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i % a = i
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inr.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ (i + a * (n / a)) % a = i

Tactic:
Int.add_mul_emod_self_left,

Goal state after:
case inr.mpr.inr.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i % a = i
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ x ∈ s, if Odd (f x) then 1 else 0) % 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})

Tactic:
simp_rw [← Finset.sum_filter, ← Nat.even_iff, Finset.card_eq_sum_ones]

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
z : Sym2 α
⊢ z ∈ m.toFinset.sym2 ↔ z ∈ m.sym2.toFinset

Tactic:
refine z.ind fun x y ↦ ?_

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
z : Sym2 α
x y : α
⊢ s(x, y) ∈ m.toFinset.sym2 ↔ s(x, y) ∈ m.sym2.toFinset
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.sym2 = image (Function.uncurry Sym2.mk) (s ×ˢ s)

Tactic:
by
  ext ⟨a, b⟩; simp; grind

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
x✝ : ∃ a, (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g) a = d
d' : β
hd : d' ∈ d
b : Sym α n
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g) b = d
⊢ ∃ a ∈ s, g a = d'

Tactic:
← hd',

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
x✝ : ∃ a, (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g) a = d
d' : β
b : Sym α n
hd : d' ∈ Sym.map (⇑g) b
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g) b = d
⊢ ∃ a ∈ s, g a = d'
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case inr
α : Type ?u.3
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = a ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = b ∨
    (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = b ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = a

Tactic:
| inr h =>

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case hl
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₁✝)) <+ map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₂✝))

Tactic:
exact ((cons_cons a h).sym n).map _

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type (max v₁ v₂ v₃)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module S Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
⊢ ∃! g', ↑R g' ∘ₗ f = g

Tactic:
exact ⟨h.lift g, h.lift_comp g, fun g' e => h.algHom_ext' _ _ (e.trans (h.lift_comp g).symm)⟩

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
⊢ homOfEq f hX hY ≍ g ↔ f ≍ g

Tactic:
cases hX; cases hY; rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X' = X
hY : Y' = Y
⊢ f ≍ homOfEq g hX hY ↔ f ≍ g

Tactic:
cases hX; cases hY; rfl

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst✝²⁰ : CommSemiring R'
inst✝¹⁹ : CommSemiring S'
inst✝¹⁸ : Algebra R R'
inst✝¹⁷ : Algebra S S'
inst✝¹⁶ : Algebra R' S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
inst✝¹³ : IsScalarTower R S S'
T' : Type u_8
inst✝¹² : CommSemiring T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
this : IsScalarTower R S T'
heq : ↑R (toAlgHom S S' T').toLinearMap ∘ₗ f = (toAlgHom R R' T').toLinearMap
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'

Tactic:
isPushout_iff,

Goal state after:
R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst✝²⁰ : CommSemiring R'
inst✝¹⁹ : CommSemiring S'
inst✝¹⁸ : Algebra R R'
inst✝¹⁷ : Algebra S S'
inst✝¹⁶ : Algebra R' S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
inst✝¹³ : IsScalarTower R S S'
T' : Type u_8
inst✝¹² : CommSemiring T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
this : IsScalarTower R S T'
heq : ↑R (toAlgHom S S' T').toLinearMap ∘ₗ f = (toAlgHom R R' T').toLinearMap
⊢ IsBaseChange T (toAlgHom R R' T').toLinearMap ↔ IsPushout S T S' T'
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst✝²⁰ : CommSemiring R'
inst✝¹⁹ : CommSemiring S'
inst✝¹⁸ : Algebra R R'
inst✝¹⁷ : Algebra S S'
inst✝¹⁶ : Algebra R' S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
inst✝¹³ : IsScalarTower R S S'
T' : Type u_8
inst✝¹² : CommSemiring T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
this : IsScalarTower R S T'
heq : ↑R (toAlgHom S S' T').toLinearMap ∘ₗ f = (toAlgHom R R' T').toLinearMap
⊢ IsBaseChange T (toAlgHom R R' T').toLinearMap ↔ IsPushout S T S' T'

Tactic:
isPushout_iff,

Goal state after:
R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst✝²⁰ : CommSemiring R'
inst✝¹⁹ : CommSemiring S'
inst✝¹⁸ : Algebra R R'
inst✝¹⁷ : Algebra S S'
inst✝¹⁶ : Algebra R' S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
inst✝¹³ : IsScalarTower R S S'
T' : Type u_8
inst✝¹² : CommSemiring T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
this : IsScalarTower R S T'
heq : ↑R (toAlgHom S S' T').toLinearMap ∘ₗ f = (toAlgHom R R' T').toLinearMap
⊢ IsBaseChange T (toAlgHom R R' T').toLinearMap ↔ IsBaseChange T (toAlgHom S S' T').toLinearMap
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map✝¹ : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map✝ : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
⊢ { preimage := f₁, map_preimage := hf₁, preimage_map := preimage_map✝¹ } =
    { preimage := f₂, map_preimage := hf₂, preimage_map := preimage_map✝ }

Tactic:
simp only [Functor.FullyFaithful.mk.injEq]

Goal state after:
case mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map✝¹ : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map✝ : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
⊢ f₁ = f₂
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
⊢ f p

Tactic:
by_cases hp : p <;> simp only [hp] <;> assumption

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case refine_1.cons
V : Type u_1
inst✝ : Quiver V
a b b✝ : V
p' : Path a b✝
e : b✝ ⟶ b
h : (p'.cons e).length ≠ 0
⊢ ∃ c p'_1 e_1, p'.cons e = p'_1.cons e_1

Tactic:
| cons p' e =>

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: case mp
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
⊢ (P.ι ⋙ F).essImage Y → P.map F Y

pp: case mpr
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
⊢ P.map F Y → (P.ι ⋙ F).essImage Y

Tactic:
· rintro ⟨X, ⟨e⟩⟩
    exact ⟨X.1, X.2, ⟨e⟩⟩

Goal state after:
case mpr
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
⊢ P.map F Y → (P.ι ⋙ F).essImage Y
Module: Mathlib.CategoryTheory.Products.Basic

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f → IsIso f.1 ∧ IsIso f.2

Tactic:
rintro ⟨g, hfg, hgf⟩
    rcases Prod.hom_ext_iff.1 hfg with ⟨hfg₁, hfg₂⟩
    rcases Prod.hom_ext_iff.1 hgf with ⟨hgf₁, hgf₂⟩
    exact ⟨⟨⟨g.1, hfg₁, hgf₁⟩⟩, ⟨⟨g.2, hfg₂, hgf₂⟩⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ G.IsEquivalence

Tactic:
isEquivalence_iff_of_iso (G.leftUnitor.symm ≪≫
    isoWhiskerRight F.asEquivalence.counitIso.symm G)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ ((F.asEquivalence.inverse ⋙ F.asEquivalence.functor) ⋙ G).IsEquivalence
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
⊢ (f ≫ f') ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) =
    (e X✝ (F_obj Y✝)) ((e X✝ (F_obj Y✝)).symm (f ≫ (e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝)))) ≫
      G.map ((e Y✝ (F_obj Z✝)).symm (f' ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))))

Tactic:
Equiv.apply_symm_apply

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
⊢ (f ≫ f') ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) =
    (f ≫ (e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫ G.map ((e Y✝ (F_obj Z✝)).symm (f' ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))))