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

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
⊢ p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : a = 0
⊢ p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors

case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
⊢ p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
⊢ k ∣ p.count a.factors

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : a = 0
⊢ k ∣ p.count a.factors

case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
⊢ k ∣ p.count a.factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case succ
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
n : ℕ
h : p.count (a ^ n).factors = n * p.count a.factors
⊢ p.count (a ^ (n + 1)).factors = (n + 1) * p.count a.factors

Tactic:
rw [pow_succ', count_mul ha (pow_ne_zero _ ha) hp, h]; ring

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : Invertible x
p : R[X]
hp : p ≠ 0
hp' : (aeval x) p = 0
⊢ IsAlgebraic R ⅟x

Tactic:
refine ⟨p.reverse, by simpa using hp, ?_⟩

Goal state after:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : Invertible x
p : R[X]
hp : p ≠ 0
hp' : (aeval x) p = 0
⊢ (aeval ⅟x) p.reverse = 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_3.inr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ (↑x)⁻¹ ∈ A

Tactic:
· rw [x_eq, Subalgebra.coe_zero, inv_zero]
      exact A.zero_mem

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z w : DirectLimit G f
i : ι
x : G i
hx : (of R ι G f i) x = z
j : ι
y : G j
hy : (of R ι G f j) y = w
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of R ι G f k) ((f j k hjk) y) = w

Tactic:
by rw [of_f, hy]

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

Goal state before:
pp: 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
q : Q
⊢ g.range ≤ Submodule.comap ((TensorProduct.mk R P Q).flip q) (rTensor Q g).range

Tactic:
by
  rintro x ⟨n, rfl⟩
  exact ⟨n ⊗ₜ[R] q, rfl⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
⊢ inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g = (lTensor Q f).range.mkQ

Tactic:
by
  rw [LinearMap.ext_iff]
  intro y
  simp only [coe_comp, Function.comp_apply, Submodule.mkQ_apply,
    lTensor.inverse_of_rightInverse_apply]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ inverse_of_rightInverse Q hfg ⋯ ∘ₗ rTensor Q g = (rTensor Q f).range.mkQ

Tactic:
rTensor.inverse_of_rightInverse_comp_rTensor

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ (rTensor Q f).range.mkQ = (rTensor Q f).range.mkQ
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : 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 : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ : DirectLimit G f
i : ι
x : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (⟦⟨i, x⟩⟧)⁻¹ = (DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧)⁻¹

Tactic:
simp_rw [inv₀_def, lift_def, map_inv₀ (g i)]

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

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝¹ : Semifield K
inst✝ : CharZero K
s : Finset ι
f : ι → K
a : K
⊢ (𝔼 i ∈ s, f i) / a = 𝔼 i ∈ s, f i / a

Tactic:
simp_rw [div_eq_mul_inv, expect_mul]

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

Goal state before:
pp: case i_inj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := F.intervalGapsWithin h a b
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij : ((p ↑i).2, (p ↑i.succ).1) = ((p ↑j).2, (p ↑j.succ).1)
⊢ i = j

Tactic:
apply F.intervalGapsWithin_injOn h a b

Goal state after:
case i_inj.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij : ((p ↑i).2, (p ↑i.succ).1) = ((p ↑j).2, (p ↑j.succ).1)
⊢ i ∈ Set.Iio k

case i_inj.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij : ((p ↑i).2, (p ↑i.succ).1) = ((p ↑j).2, (p ↑j.succ).1)
⊢ j ∈ Set.Iio k

case i_inj.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij : ((p ↑i).2, (p ↑i.succ).1) = ((p ↑j).2, (p ↑j.succ).1)
⊢ (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) i =
    (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case add
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x✝ y✝ : M₁ ⊗[R] M₂
a✝¹ : motive ((TensorProduct.lift f) x✝)
a✝ : motive ((TensorProduct.lift f) y✝)
⊢ motive ((TensorProduct.lift f) (x✝ + y✝))

Tactic:
rw [map_add]
    apply add <;> assumption

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

Goal state before:
pp: α : Type u_1
x : α
xs : List α
z : Sym2 α
⊢ z = s(x, x) ∨ (∃ a ∈ xs, s(x, a) = z) ∨ z ∈ xs.sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2

Tactic:
simp only [eq_comm]

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

Goal state before:
pp: α : Type u_1
s : Finset α
m : Sym2 α
⊢ m ∈ s.val.sym2 ↔ ∀ a ∈ m, a ∈ s

Tactic:
Multiset.mem_sym2_iff

Goal state after:
α : Type u_1
s : Finset α
m : Sym2 α
⊢ (∀ y ∈ m, y ∈ s.val) ↔ ∀ a ∈ m, a ∈ s
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s.sym2 = (#s + 1).choose 2

Tactic:
card_def,

Goal state after:
α : Type u_1
s : Finset α
⊢ s.sym2.val.card = (#s + 1).choose 2
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (s.val.card + 1).choose 2 = (#s + 1).choose 2

Tactic:
← card_def

Goal state after:
α : Type u_1
s : Finset α
⊢ (#s + 1).choose 2 = (#s + 1).choose 2
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, g a_2 = a
g' : { x // x ∈ d } → α :=
  fun x ↦
    match x with
    | ⟨x, hx⟩ => ⋯.choose
⊢ Sym.map (fun x ↦ g ⋯.choose) d.attach = d

Tactic:
convert! Sym.attach_map_coe d with ⟨x, hx⟩ hx'

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, g a_2 = a
g' : { x // x ∈ d } → α :=
  fun x ↦
    match x with
    | ⟨x, hx⟩ => ⋯.choose
x : β
hx : x ∈ d
hx' : ⟨x, hx⟩ ∈ d.attach
⊢ g ⋯.choose = ↑⟨x, hx⟩
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ Fin (n + 1) → Type ?u.73

pp: case refine_2
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ (a : Fin (n + 1)) → ↥(s.sym (n - ↑a)) → ?refine_1 (id a)

pp: case refine_3
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i✝ : Fin (n + 1)
m : Sym α (n - ↑i✝)
hm : m ∈ s.sym (n - ↑i✝)
i : Fin (n + 1)
⊢ Function.Injective (?refine_2 i)

pp: case refine_4
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ Sigma.map id ?refine_2
      ((fun m ↦ ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩)
        ((fun m ↦ ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩)) =
    Sigma.map id ?refine_2 ⟨i, ⟨m, hm⟩⟩

Tactic:
· exact fun i ↦ Sym α (n - i)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ (a : Fin (n + 1)) → ↥(s.sym (n - ↑a)) → Sym α (n - ↑(id a))

case refine_3
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i✝ : Fin (n + 1)
m : Sym α (n - ↑i✝)
hm : m ∈ s.sym (n - ↑i✝)
i : Fin (n + 1)
⊢ Function.Injective (?refine_2 i)

case refine_4
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ Sigma.map id ?refine_2
      ((fun m ↦ ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩)
        ((fun m ↦ ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩)) =
    Sigma.map id ?refine_2 ⟨i, ⟨m, hm⟩⟩
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
⊢ ∀ (a₁ : α × α) (b₁ : β × β) (a₂ : α × α) (b₂ : β × β),
    a₁ ≈ a₂ → b₁ ≈ b₂ → ↑f a₁.1 a₁.2 b₁.1 b₁.2 = ↑f a₂.1 a₂.2 b₂.1 b₂.2

Tactic:
by
        rintro _ _ _ _ ⟨⟩ ⟨⟩
        exacts [rfl, (f.2 _ _ _ _).2, (f.2 _ _ _ _).1, (f.2 _ _ _ _).1.trans (f.2 _ _ _ _).2]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
⊢ Q

Tactic:
let _ := I₃

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
x✝ : Module R Q := I₃
⊢ Q
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
⊢ ∏ j ∈ s, f j = ⊤ ↔ (∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0

Tactic:
by
  constructor
  · exact fun h ↦ ⟨prod_eq_top_ex_top h, fun _ ih ↦ prod_eq_top_ne_zero ih h⟩
  · exact fun ⟨h, h'⟩ ↦ prod_eq_top (Exists.choose_spec h).1 (Exists.choose_spec h).2 h'

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

Goal state before:
pp: α : Type u_1
e : Sym2 α
⊢ e = s((Quot.out e).1, (Quot.out e).2)

Tactic:
Sym2.mk,

Goal state after:
α : Type u_1
e : Sym2 α
⊢ e = Quot.mk (Rel α) ((Quot.out e).1, (Quot.out e).2)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
z : Sym2 α
⊢ x ∈ z.toMultiset.toFinset ↔ x ∈ z.toMultiset

Tactic:
Multiset.mem_toFinset

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
z : Sym2 α
⊢ x ∈ z.toMultiset ↔ x ∈ z.toMultiset
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ s(x, y).toFinset = {x, y}

Tactic:
by
  ext; simp [← Sym2.mem_toFinset, ← Sym2.mem_iff]

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

Goal state before:
pp: α : Type u_1
s : Set α
z : Sym2 α
⊢ z ∈ s.sym2 ↔ ↑z ⊆ s

Tactic:
induction z using Sym2.inductionOn

Goal state after:
case hf
α : Type u_1
s : Set α
x✝ y✝ : α
⊢ s(x✝, y✝) ∈ s.sym2 ↔ ↑s(x✝, y✝) ⊆ s
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
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'

Tactic:
have : IsScalarTower R S T' := .of_algebraMap_eq fun x ↦ by
    rw [algebraMap_apply R S' T', algebraMap_apply R S S', ← algebraMap_apply S S' T']

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'
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'
Module: Mathlib.CategoryTheory.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : C
f g : X ⟶ Y
h : (fun f ↦ ⇑(hom f)) f = (fun f ↦ ⇑(hom f)) g
⊢ f = g

Tactic:
rw [← ofHom_hom f, ← ofHom_hom g]
    simp_all

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

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₂ : Path b b
hq : nil.length = q₂.length
h : p₁.comp nil = p₂.comp q₂
⊢ p₁ = p₂ ∧ nil = q₂

Tactic:
rcases q₂ with _ | ⟨q₂, f₂⟩

Goal state after:
case nil.nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
hq : nil.length = nil.length
h : p₁.comp nil = p₂.comp nil
⊢ p₁ = p₂ ∧ nil = nil

case nil.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ b
hq : nil.length = (q₂.cons f₂).length
h : p₁.comp nil = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ nil = q₂.cons f₂
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ c✝ : V
q₁ : Path b b✝
f₁ : b✝ ⟶ c✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
q₂ : Path b c✝
hq : (q₁.cons f₁).length = q₂.length
h : p₁.comp (q₁.cons f₁) = p₂.comp q₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂

Tactic:
rcases q₂ with _ | ⟨q₂, f₂⟩

Goal state after:
case cons.nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₁ : Path b b✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
f₁ : b✝ ⟶ b
hq : (q₁.cons f₁).length = nil.length
h : p₁.comp (q₁.cons f₁) = p₂.comp nil
⊢ p₁ = p₂ ∧ q₁.cons f₁ = nil

case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝¹ c✝ : V
q₁ : Path b b✝¹
f₁ : b✝¹ ⟶ c✝
ih : ∀ {q₂ : Path b b✝¹}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : p₁.comp (q₁.cons f₁) = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ Dᵒᵖ
e : F ≅ G
X : C
⊢ (e.inv.app X ≫ e.hom.app X).unop = 𝟙 (Opposite.unop (G.obj X))

Tactic:
inv_hom_id_app,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ Dᵒᵖ
e : F ≅ G
X : C
⊢ (𝟙 (G.obj X)).unop = 𝟙 (Opposite.unop (G.obj X))
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
⊢ (f ≫ fun i ↦ Groupoid.inv (f i)) = 𝟙 X✝

Tactic:
funext i; apply Groupoid.comp_inv

Goal state after:
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: case mp
X Y : Type u
f : X → Y
⊢ Mono (↾f) → Function.Injective f

Tactic:
intro H x x' h
    rw [← homOfElement_eq_iff] at h ⊢
    exact (cancel_mono (ofHom f)).mp h

Goal state after:
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: case mpr
X Y : Type u
f : X → Y
⊢ Function.Injective f → Mono (↾f)

Tactic:
refine fun H => ⟨fun g g' h => ConcreteCategory.hom_ext _ _ fun x ↦
      congrFun (H.comp_left ?_) x⟩
    ext y
    exact ConcreteCategory.congr_hom h y

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
⊢ P.inverseImage E.functor ≤ P.map E.inverse

pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
⊢ P.map E.inverse ≤ P.inverseImage E.functor

Tactic:
· intro X Y f hf
    refine ⟨_, _, _, hf, ⟨?_⟩⟩
    exact ((Functor.mapArrowFunctor _ _).mapIso E.unitIso.symm).app (Arrow.mk f)

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
⊢ P.map E.inverse ≤ P.inverseImage E.functor
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
adj : CoreUnitCounit F G
Y : D
⊢ adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)

Tactic:
have := adj.right_triangle

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
adj : CoreUnitCounit F G
Y : D
this : G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G = NatTrans.id (G ⋙ 𝟭 C)
⊢ adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
Y : C
e : yoneda.obj Y ≅ F
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ (e.app (op X)).toEquiv (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) ((e.app (op X')).toEquiv g)

Tactic:
by apply e.hom.naturality_apply

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
X✝ : C
e : coyoneda.obj (op X✝) ≅ F
X X' : C
f : X ⟶ X'
g : X✝ ⟶ X
⊢ (e.app X').toEquiv (g ≫ f) = (ConcreteCategory.hom (F.map f)) ((e.app X).toEquiv g)

Tactic:
by apply e.hom.naturality_apply

Goal state after: