mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)

Tactic:
rw [pairwise_cons']

Goal state after:
case cons
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) ↔
    Pairwise (IsCoprime on fun a ↦ s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons.mp
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) →
    Pairwise (IsCoprime on fun a ↦ s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

Tactic:
rintro ⟨μ, hμ⟩
      rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat] at hμ
      refine ⟨ih.mp ⟨Pi.single h.choose (μ a * s h.choose) + μ * fun _ ↦ s a, ?_⟩, fun b hb ↦ ?_⟩
      · rw [prod_eq_mul_prod_sdiff_singleton_of_mem h.choose_spec, ← mul_assoc, ←
          @if_pos _ _ h.choose_spec R (_ * _) 0, ← sum_pi_single', ← sum_add_distrib] at hμ
        rw [← hμ, sum_congr rfl]
        intro x hx
        convert! add_mul (R := R) _ _ _ using 2
        · by_cases hx : x = h.choose
          · rw [hx, Pi.single_eq_same, Pi.single_eq_same]
          · rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]
        · convert! (mul_assoc _ _ _).symm
          rw [prod_eq_prod_sdiff_singleton_mul (mem x hx), mul_comm, sdiff_sdiff_comm,
            sdiff_singleton_eq_erase a, erase_insert hat]
      · have : IsCoprime (s b) (s a) :=
          ⟨μ a * ∏ i ∈ t \ {b}, s i, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j, ?_⟩
        · exact ⟨this.symm, this⟩
        rw [mul_assoc, ← prod_eq_prod_sdiff_singleton_mul hb, sum_mul, ← hμ, sum_congr rfl]
        intro x hx
        rw [mul_assoc]
        congr
        rw [prod_eq_prod_sdiff_singleton_mul (mem x hx) _]
        congr 2
        rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)

Tactic:
rw [pairwise_cons']
    have mem : ∀ x ∈ t, a ∈ insert a t \ {x} := fun x hx ↦ by
      rw [mem_sdiff, mem_singleton]
      exact ⟨mem_insert_self _ _, fun ha ↦ hat (ha ▸ hx)⟩
    constructor
    · rintro ⟨μ, hμ⟩
      rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat] at hμ
      refine ⟨ih.mp ⟨Pi.single h.choose (μ a * s h.choose) + μ * fun _ ↦ s a, ?_⟩, fun b hb ↦ ?_⟩
      · rw [prod_eq_mul_prod_sdiff_singleton_of_mem h.choose_spec, ← mul_assoc, ←
          @if_pos _ _ h.choose_spec R (_ * _) 0, ← sum_pi_single', ← sum_add_distrib] at hμ
        rw [← hμ, sum_congr rfl]
        intro x hx
        convert! add_mul (R := R) _ _ _ using 2
        · by_cases hx : x = h.choose
          · rw [hx, Pi.single_eq_same, Pi.single_eq_same]
          · rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]
        · convert! (mul_assoc _ _ _).symm
          rw [prod_eq_prod_sdiff_singleton_mul (mem x hx), mul_comm, sdiff_sdiff_comm,
            sdiff_singleton_eq_erase a, erase_insert hat]
      · have : IsCoprime (s b) (s a) :=
          ⟨μ a * ∏ i ∈ t \ {b}, s i, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j, ?_⟩
        · exact ⟨this.symm, this⟩
        rw [mul_assoc, ← prod_eq_prod_sdiff_singleton_mul hb, sum_mul, ← hμ, sum_congr rfl]
        intro x hx
        rw [mul_assoc]
        congr
        rw [prod_eq_prod_sdiff_singleton_mul (mem x hx) _]
        congr 2
        rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]
    · rintro ⟨hs, Hb⟩
      obtain ⟨μ, hμ⟩ := ih.mpr hs
      obtain ⟨u, v, huv⟩ := IsCoprime.prod_left fun b hb ↦ (Hb b hb).right
      use fun i ↦ if i = a then u else v * μ i
      have hμ' : (∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a)) = v * s a := by
        rw [← mul_sum, ← sum_mul, hμ, one_mul]
      rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat]
      simp only [↓reduceIte, ite_mul]
      rw [← huv, ← hμ', sum_congr rfl]
      intro x hx
      rw [mul_assoc, if_neg fun ha : x = a ↦ hat (ha.casesOn hx)]
      rw [mul_assoc]
      congr
      rw [prod_eq_prod_sdiff_singleton_mul (mem x hx) _]
      congr 2
      rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t : Finset I
⊢ IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x

Tactic:
refine Finset.induction_on t (iff_of_true isRelPrime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_

Goal state after:
α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
⊢ IsRelPrime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsRelPrime (s i) x
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i ∈ ∅, span R (M i) = span R (∏ i ∈ ∅, M i)

Tactic:
simp [one_eq_span, Set.singleton_one]

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

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
⊢ span R (SetSemiring.down 0) * P = 0

Tactic:
SetSemiring.down_zero,

Goal state after:
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
⊢ span R ∅ * P = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b c : R
hb : b ≠ 0
h : a * b = c
⊢ a = a * b / b

Tactic:
mul_div_cancel_right₀ _ hb

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hb : b ≠ 0
h : a * b = c
⊢ a = a
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type u_1
inst✝⁶ : Semiring R✝
inst✝⁵ : Semiring S
inst✝⁴ : FunLike F R✝ S
f : F
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R✝
inst✝² : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : Finite ι
I : Ideal ((i : ι) → R i)
⊢ pi ((fun I i ↦ map (Pi.evalRingHom R i) I) I) = I

Tactic:
ext r
      simp_rw [mem_pi, mem_map_iff_of_surjective (Pi.evalRingHom R _) (Function.surjective_eval _)]
      refine ⟨(fun ⟨r', hr'⟩ ↦ ?_) ∘ Classical.skolem.mp, fun hr i ↦ ⟨r, hr, rfl⟩⟩
      have := Fintype.ofFinite ι
      classical rw [show r = ∑ i, Pi.single i 1 * r' i from funext fun i ↦ by
        rw [← (hr' _).2, Finset.sum_apply, Fintype.sum_eq_single i fun j ne ↦ by simp [ne]]; simp]
      exact sum_mem fun i _ ↦ I.mul_mem_left _ (hr' i).1

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type u_1
inst✝⁷ : Semiring R✝
inst✝⁶ : Semiring S
inst✝⁵ : FunLike F R✝ S
f : F
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝⁴ : FunLike G S R✝
inst✝³ : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝² : (i : ι) → Semiring (R i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsPrincipalIdealRing (R i)
I : Ideal ((i : ι) → R i)
⊢ Submodule.IsPrincipal I

Tactic:
← piOrderIso.symm_apply_apply I

Goal state after:
R✝ : Type u
S : Type v
F : Type u_1
inst✝⁷ : Semiring R✝
inst✝⁶ : Semiring S
inst✝⁵ : FunLike F R✝ S
f : F
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝⁴ : FunLike G S R✝
inst✝³ : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝² : (i : ι) → Semiring (R i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsPrincipalIdealRing (R i)
I : Ideal ((i : ι) → R i)
⊢ Submodule.IsPrincipal (piOrderIso.symm (piOrderIso I))
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
this : ∀ I ∈ A, y ∈ map f I
J : Submodule R R
⊢ J ∈ A → x ∈ J

Tactic:
hJ

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
this : ∀ I ∈ A, y ∈ map f I
J : Submodule R R
hJ : J ∈ A
⊢ x ∈ J
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ z * ↑(if 0 ≤ z then 1 else -1) = -z

Tactic:
if_neg (not_le_of_gt h),

Goal state after:
case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ z * ↑(-1) = -z
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ ↑u * ↑(Exists.choose ⋯) = ↑(Exists.choose ⋯)

Tactic:
← (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero ha).eq_iff,

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ a * (↑u * ↑(Exists.choose ⋯)) = a * ↑(Exists.choose ⋯)
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : b ∉ s
hi : (∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd (s.gcd g) (GCDMonoid.gcd a (f b)) = GCDMonoid.gcd (GCDMonoid.gcd (g b) (s.gcd g)) a

Tactic:
gcd_comm (g b),

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : b ∉ s
hi : (∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd (s.gcd g) (GCDMonoid.gcd a (f b)) = GCDMonoid.gcd (GCDMonoid.gcd (s.gcd g) (g b)) a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ gcd a b = 0

Tactic:
by
    rw [ha, hb, ← zero_dvd_iff]
    apply dvd_gcd <;> rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, IsCoprime I (J j)
⊢ IsCoprime I (⨅ j ∈ s, J j)

Tactic:
simp only [isCoprime_iff_add, one_eq_top] at hf ⊢
  exact sup_iInf_eq_top hf

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (factors a).prod ~ᵤ a

Tactic:
rw [factors, dif_neg ane0]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Classical.choose ⋯).prod ~ᵤ a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
have h : gcd a b ≠ 0 := fun H => h1 ((gcd_eq_zero_iff _ _).1 H).1

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h✝ : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : gcd a b ≠ 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
⊢ ∀ (a b : Associates α), Quotient.map₂ gcd ⋯ a b ∣ a

Tactic:
by rintro ⟨a⟩ ⟨b⟩; exact mk_le_mk_of_dvd (gcd_dvd_left _ _)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : ¬f b ≤ f i
Hi : I ≤ f i
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
exact Or.inr (Or.inr ⟨i, Finset.mem_insert_self i t, Hi⟩)

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j ↦ ↑(v.repr ↑j).support
S' : ↑J → Set M := fun j ↦ ⇑v '' S j
b : M
hb : b ∈ range ⇑v
i : ι
hi : v i = b
this : span R J ≤ comap (↑v.repr) (Finsupp.supported R R (⋃ j, S j))
⊢ b ∈ ⋃ j, S' j

Tactic:
hJ

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j ↦ ↑(v.repr ↑j).support
S' : ↑J → Set M := fun j ↦ ⇑v '' S j
b : M
hb : b ∈ range ⇑v
i : ι
hi : v i = b
this : ⊤ ≤ comap (↑v.repr) (Finsupp.supported R R (⋃ j, S j))
⊢ b ∈ ⋃ j, S' j
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
v : Basis ι R M
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} (Module.rank R M)

Tactic:
have := nontrivial_of_invariantBasisNumber R
  rw [← v.mk_range_eq_rank, Cardinal.mk_range_eq_of_injective v.injective]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a (insert b u)), ↑(f i)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
i : ι
⊢ i ∈ u → (f i).IsPrime

Tactic:
hiu

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a (insert b u)), ↑(f i)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
i : ι
hiu : i ∈ u
⊢ (f i).IsPrime
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocRing α
v w : m → α
⊢ -v ⬝ᵥ -w = v ⬝ᵥ w

Tactic:
neg_dotProduct,

Goal state after:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocRing α
v w : m → α
⊢ -(v ⬝ᵥ -w) = v ⬝ᵥ w
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case inr.inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j k : n
hkl : j ≠ k
⊢ diagonal (fun x ↦ M i i) j k = M j k

Tactic:
rw [diagonal_apply_ne _ hkl]
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [col_eq_zero_of_commute_single (hM hkl.symm) hkl]
    · rw [row_eq_zero_of_commute_single (hM hij) hkl.symm]

Goal state after:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
x : ↑T
i : ι
hx : ↑x ∈ S i
⊢ iUnionLift S f hf T hT x = f i ⟨↑x, hx⟩

Tactic:
obtain ⟨x, hx⟩ := x; exact hf _ _ _ _ _

Goal state after:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
t : Set β
⊢ iUnionLift S f hf T hT ⁻¹' t = inclusion hT ⁻¹' ⋃ i, inclusion ⋯ '' f i ⁻¹' t

Tactic:
by
  ext x
  simp only [mem_preimage, mem_iUnion, mem_image]
  constructor
  · rcases mem_iUnion.1 (hT x.prop) with ⟨i, hi⟩
    refine fun h => ⟨i, ⟨x, hi⟩, ?_, rfl⟩
    rwa [iUnionLift_of_mem x hi] at h
  · rintro ⟨i, ⟨y, hi⟩, h, hxy⟩
    obtain rfl : y = x := congr_arg Subtype.val hxy
    rwa [iUnionLift_of_mem x hi]

Goal state after:
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α✝ : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : NonAssocSemiring α✝
inst✝³ : NonAssocSemiring β
inst✝² : NonAssocSemiring γ
α : Type ?u.30
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
x✝¹ x✝ : Matrix m m αᵐᵒᵖ
⊢ unop (op ((x✝¹ * x✝)ᵀ.map unop)) = unop (op (x✝¹ᵀ.map unop) * op (x✝ᵀ.map unop))

Tactic:
ext; simp [mul_apply]

Goal state after:
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: α : Type u_14
inst✝¹ : MulOne α
inst✝ : AddCommMonoid α
x✝² : IsStablyFiniteRing αᵐᵒᵖ
n : ℕ
x✝¹ x✝ : Matrix (Fin n) (Fin n) α
⊢ { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun (x✝¹ * x✝) =
    { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝¹ *
      { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝

Tactic:
ext; simp [mul_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
hx : x ∈ I
⊢ x * y ∈ I

Tactic:
simpa using! I.ringCon.mul hx (I.ringCon.refl y)

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ Equivalence fun x y ↦ f x = f y

Tactic:
by constructor <;> aesop

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤

Tactic:
by
    ext x; exact ⟨fun _ => mem_top, fun _ => h x⟩

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝² : CommSemiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
S T : NonUnitalSubalgebra R A
h : (fun S ↦ S.toSubmodule) S = (fun S ↦ S.toSubmodule) T
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T

Tactic:
by apply SetLike.ext_iff.1 h

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝² : CommSemiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
S T : NonUnitalSubalgebra R A
h : (fun S ↦ S.toNonUnitalSubsemiring) S = (fun S ↦ S.toNonUnitalSubsemiring) T
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T

Tactic:
by apply SetLike.ext_iff.1 h

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝² : CommRing R
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : Module R A
S T : NonUnitalSubalgebra R A
h : (fun S ↦ S.toNonUnitalSubring) S = (fun S ↦ S.toNonUnitalSubring) T
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T

Tactic:
by apply SetLike.ext_iff.1 h

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: case mk.mk
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
toSubsemiring✝¹ : Subsemiring A
algebraMap_mem'✝¹ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝

Tactic:
exact SetLike.coe_injective h

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
a✝ b✝ : A
w✝¹ : a✝ ∈ adjoin R s
hpx : p a✝ w✝¹
w✝ : b✝ ∈ adjoin R s
hpy : p b✝ w✝
⊢ a✝ * b✝ ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx}

Tactic:
exact ⟨_, mul _ _ _ _ hpx hpy⟩

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

Goal state before:
pp: case invFun
R : Type u
inst✝¹⁶ : CommSemiring R
S : Type ?u.6
inst✝¹⁵ : Semiring S
inst✝¹⁴ : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst✝¹³ : DecidableEq ι₁
inst✝¹² : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝¹¹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝¹⁰ : AddCommMonoid M₁'
inst✝⁹ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝⁸ : AddCommMonoid M₂'
inst✝⁷ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝⁶ : Module R M₁'
inst✝⁵ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝⁴ : Module R M₂'
inst✝³ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝² : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
⊢ (⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) →ₗ[S] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂

Tactic:
exact toModule S _ _ fun i => AlgebraTensorModule.map (lof S _ M₁ i.1) (lof R _ M₂ i.2)

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
i : ι
n : N
⊢ (finsuppScalarLeft R N ι).symm (Finsupp.single i n) = Finsupp.single i 1 ⊗ₜ[R] n

Tactic:
simp [finsuppScalarLeft, finsuppLeft_symm_apply_single]

Goal state after:
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
a u : R
hu : IsUnit u
⊢ IsSelfAdjoint (u * a * star u) ↔ IsSelfAdjoint a

Tactic:
by
  simp [IsSelfAdjoint, mul_assoc, hu.mul_right_inj, hu.star.mul_left_inj]

Goal state after: