mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x r s g : R
hr : x = g * r
hgxy : ¬g = 0
hxy : x = 0 ∨ g * s / gcd x (g * s) = 0
hy : s = 0
⊢ g * s = 0

Tactic:
hy,

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x r s g : R
hr : x = g * r
hgxy : ¬g = 0
hxy : x = 0 ∨ g * s / gcd x (g * s) = 0
hy : s = 0
⊢ g * 0 = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case mpr.inr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hy : y = 0
⊢ lcm x y = 0

Tactic:
hy,

Goal state after:
case mpr.inr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hy : y = 0
⊢ lcm x 0 = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr.refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
x y : M
hx✝ : x ∈ span R s
hy✝ : y ∈ span R s
hx : r • x = 0
hy : r • y = 0
⊢ 0 + r • y = 0

Tactic:
hy,

Goal state after:
case mpr.refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
x y : M
hx✝ : x ∈ span R s
hy✝ : y ∈ span R s
hx : r • x = 0
hy : r • y = 0
⊢ 0 + 0 = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ comap f (map f I) = comap f (map f J) ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f

Tactic:
comap_map_of_surjective f hf,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ I ⊔ comap f ⊥ = comap f (map f J) ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ I ⊔ comap f ⊥ = comap f (map f J) ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f

Tactic:
comap_map_of_surjective f hf,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ I ⊔ comap f ⊥ = J ⊔ comap f ⊥ ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
a : α
ha : a ∈ b * ↑u ::ₘ f.erase b
⊢ Irreducible a

pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ (b * ↑u ::ₘ f.erase b).prod = f.prod * ↑u

Tactic:
· obtain rfl | ha := Multiset.mem_cons.1 ha
        exacts [Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ (b * ↑u ::ₘ f.erase b).prod = f.prod * ↑u
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
x✝ : a ∣ 1 ∧ b ∣ 1
c : α
hc : 1 = a * c
d : α
hd : 1 = b * d
⊢ lcm ↑(Units.mkOfMulEqOne a c ⋯) ↑(Units.mkOfMulEqOne b d ⋯) = 1

Tactic:
rw [lcm_units_coe_left, normalize_coe_units]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
s : Finset α
f : α → R
⊢ ∃ g, s.gcd f = ∑ a ∈ s, f a * g a

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    obtain ⟨x, y, hxy⟩ := IsBezout.gcd_eq_sum (f a) (s.gcd f)
    obtain ⟨u, hu⟩ := IsBezout.associated_gcd_gcd R (x := f a) (y := s.gcd f)
    rw [← hxy, add_mul, mul_comm x, mul_comm y] at hu
    obtain ⟨g, hg⟩ := ih
    refine ⟨Function.update (g · * (y * u)) a (x * u), ?_⟩
    rw [gcd_insert, sum_insert ha, ← hu, hg]
    simp only [Function.update_self, add_right_inj, sum_mul, mul_assoc]
    exact sum_congr rfl fun b hb ↦ congrArg (f b * ·) <|
      (Function.update_of_ne (show b ≠ a by grind) (x * u) (g · * (y * u))).symm

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S * 1 = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T

Tactic:
hy,

Goal state after:
case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
h : z ∈ S
y : R
hz : generator S * 1 = generator T * (generator S * y)
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
⊢ Associated (normalize (Classical.choose ⋯) * lcm a b) (a * b)

Tactic:
rw [mul_comm]

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
⊢ Associated (lcm a b * normalize (Classical.choose ⋯)) (a * b)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case i.hg
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : RankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective ⇑↑b.repr

Tactic:
apply LinearEquiv.surjective

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
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ #ι ≤ #↑↑⟨range ⇑v, ⋯⟩

Tactic:
· exact (Cardinal.mk_range_eq v v.injective).ge

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : StrongRankCondition R
h : Bijective ⇑(algebraMap R S)
⊢ finrank R S = 1

Tactic:
by
  rw [← (AlgEquiv.ofBijective (Algebra.ofId R S) h).toLinearEquiv.finrank_eq, finrank_self]

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

Goal state before:
pp: case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ ∃ i ∈ t, I ≤ f i
has : a ∈ insert a t
hbt : b ∉ t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert a t, I ≤ f i

Tactic:
rwa [Finset.exists_mem_insert]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ StrongRankCondition R ↔ ∀ n > 0, 0 < finrank R (Fin n → R)

Tactic:
rw [strongRankCondition_iff_forall_rank_lt_aleph0, ← not_iff_not]

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (¬∀ (n : ℕ), Module.rank R (Fin n → R) < ℵ₀) ↔ ¬∀ n > 0, 0 < finrank R (Fin n → R)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
inst✝ : Module.Finite K ↥(span K s)
⊢ ∃ t, ↑t ⊆ s ∧ t.card = finrank K ↥(span K s) ∧ span K ↑t = span K s ∧ LinearIndepOn K id ↑t

Tactic:
by
  rcases exists_linearIndependent K s with ⟨t, ht_sub, ht_span, ht_indep⟩
  obtain ⟨t, rfl, ht_card⟩ : ∃ u : Finset M, ↑u = t ∧ u.card = finrank K (span K s) := by
    rw [← Cardinal.mk_set_eq_nat_iff_finset, finrank_eq_rank, ← ht_span, rank_span_set ht_indep]
  exact ⟨t, ht_sub, ht_card, ht_span, ht_indep⟩

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
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert b t
hbs : b ∈ insert b t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert b t, I ≤ f i

Tactic:
rwa [Finset.exists_mem_insert]

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

Goal state before:
pp: case neg.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : I ≤ f i ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
rwa [Finset.exists_mem_insert]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ ((Finsupp.mapRange Subtype.val ⋯ f).sum fun i a ↦ a • v i) = f.sum fun i x ↦ ↑x • v i

Tactic:
Finsupp.sum_mapRange_index

Goal state after:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ (f.sum fun a b ↦ ↑b • v a) = f.sum fun i x ↦ ↑x • v i

ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ ∀ (a : ι), 0 • v a = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (if h : 0 ∈ I then ⟨0, h⟩ else 0) = 0

Tactic:
simp only [Submodule.zero_mem, ↓reduceDIte]; rfl

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ((Finsupp.mapRange (fun r ↦ if h : r ∈ I then ⟨r, h⟩ else 0) ⋯ a).sum fun i x ↦ ↑x • v i) = a.sum fun i c ↦ c • v i

Tactic:
Finsupp.sum_mapRange_index

Goal state after:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun a b ↦ ↑(if h : b ∈ I then ⟨b, h⟩ else 0) • v a) = a.sum fun i c ↦ c • v i

ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∀ (a : ι), ↑0 • v a = 0
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Subsingleton R
⊢ Finite (ChooseBasisIndex R M)

Tactic:
have := Module.subsingleton R M
    rw [ChooseBasisIndex]
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
⊢ count x s = s.card * if x = a then 1 else 0

Tactic:
simp_rw [hx, ite_true, mul_one, count_eq_card]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
⊢ ∀ x ∈ s, a = x
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Sort u_3
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⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
this : x = inclusion ⋯ ⟨↑x, hi⟩
| iUnionLift S f hf (iUnion S) ⋯ (inclusion ⋯ (ui i ⟨↑x, hi⟩))

Tactic:
iUnionLift_inclusion

Goal state after:
α : Type u_1
ι : Sort u_2
β : Sort u_3
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⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
this : x = inclusion ⋯ ⟨↑x, hi⟩
| f i (ui i ⟨↑x, hi⟩)
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Sort u_3
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⟩
dir : Directed (fun x1 x2 ↦ x1 ⊆ x2) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ⊆ S k
hjk : S j ⊆ S k
hx : x = inclusion ⋯ ⟨↑x, ⋯⟩
hy : y = inclusion ⋯ ⟨↑y, ⋯⟩
hxy : ↑(inclusion ⋯ (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)) ∈ S k
| iUnionLift S f hf (iUnion S) ⋯ (op (inclusion ⋯ ⟨↑x, ⋯⟩) y)

Tactic:
hy,

Goal state after:
α : Type u_1
ι : Sort u_2
β : Sort u_3
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⟩
dir : Directed (fun x1 x2 ↦ x1 ⊆ x2) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ⊆ S k
hjk : S j ⊆ S k
hx : x = inclusion ⋯ ⟨↑x, ⋯⟩
hy : y = inclusion ⋯ ⟨↑y, ⋯⟩
hxy : ↑(inclusion ⋯ (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)) ∈ S k
| iUnionLift S f hf (iUnion S) ⋯ (op (inclusion ⋯ ⟨↑x, ⋯⟩) (inclusion ⋯ ⟨↑y, ⋯⟩))
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case refine_3
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : FunLike F A B
inst✝² : NonUnitalAlgHomClass F R A B
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (x y : A),
    x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
      y ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
        x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
          y * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
            (x + y) * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

Tactic:
exact fun x y _ _ => (add_mul x y b).symm ▸ add_mem

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
x : M
i j : ι
hij : i ≠ j
a : α j
hx : x ∈ A i
⊢ ((h.collectedBasis v).repr x) ⟨j, a⟩ = 0

Tactic:
by
  change (sigmaFinsuppLequivDFinsupp R).symm (DFinsupp.mapRange _ (fun i ↦ map_zero _) _) _ = _
  simp [h.ofBijective_coeLinearMap_of_mem_ne hij hx]

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
a b : A
s : Set A
hb : b ∈ adjoin R s
h : ∀ b ∈ s, Commute a b
⊢ Commute a b

Tactic:
induction hb using adjoin_induction with

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
⊢ (∃ s, ∀ (x : P), (linearCombination R id) (s x) = x) ↔ ∃ s, ∀ (x : P), (linearCombination R id) (s x) = LinearMap.id x

Tactic:
id_apply

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
P : Type v
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Small.{w, u} R
inst✝ : Small.{w, v} P
e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R := ⋯
x✝ : Projective R P
i : P →ₗ[R] P →₀ R
hi : Function.LeftInverse ⇑(linearCombination R id) ⇑i
⊢ ∀ (x : P), ((linearCombination R id ∘ₗ ↑e) ∘ₗ ↑e.symm ∘ₗ i) x = LinearMap.id x

Tactic:
simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, e.apply_symm_apply]

Goal state after:
R : Type u
inst✝⁴ : Semiring R
P : Type v
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Small.{w, u} R
inst✝ : Small.{w, v} P
e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
  mapDomain.linearEquiv (Shrink.{w, u} R) R (equivShrink P).symm ≪≫ₗ mapRange.linearEquiv (Shrink.linearEquiv R R)
x✝ : Projective R P
i : P →ₗ[R] P →₀ R
hi : Function.LeftInverse ⇑(linearCombination R id) ⇑i
⊢ ∀ (x : P), (linearCombination R id) (i x) = LinearMap.id x
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x y : R
hx : star x = -x
hy : star y = -y
⊢ -x + star y = -(x + y)

Tactic:
hy,

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x y : R
hx : star x = -x
hy : star y = -y
⊢ -x + -y = -(x + y)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
⊢ a * star a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)

Tactic:
hb.eq,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
⊢ a * star a + star b * a + (star a * b + b * star b) = a * star a + b * star a + (a * star b + b * star b)
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
⊢ (selfAdjointPart R).prod (skewAdjointPart R) ∘ₗ
      (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype =
    LinearMap.id

Tactic:
ext x <;> dsimp <;> erw [Submodule.coe_subtype, Submodule.coe_subtype] <;> simp

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

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
inst✝² : DecidableEq o
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : (i : o) → Matrix (m' i) (n' i) α
⊢ (blockDiagonal' fun k ↦ (M k)ᵀ).map star = blockDiagonal' fun k ↦ (M k)ᵀ.map star

Tactic:
exact blockDiagonal'_map _ star (star_zero α)

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
⊢ generator (ϕ.submoduleImage N) ∣ ψ ⟨y, ⋯⟩

Tactic:
refine dvd_trans ?_ d_dvd_right

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
⊢ generator (ϕ.submoduleImage N) ∣ d
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ baseChange A p ≤ span A ↑(map ((TensorProduct.mk R A M) 1) p)

pp: case refine_2
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ span A ↑(map ((TensorProduct.mk R A M) 1) p) ≤ baseChange A p

Tactic:
· rw [baseChange, LinearMap.range_le_iff_comap, eq_top_iff,
      ← span_eq_top_of_span_eq_top R A _ (span_tmul_eq_top R ..), span_le]
    refine fun _ ⟨a, m, h⟩ ↦ ?_
    rw [← h, SetLike.mem_coe, mem_comap, LinearMap.baseChange_tmul, ← mul_one a, ← smul_eq_mul,
      ← smul_tmul']
    exact smul_mem _ a (subset_span ⟨m, m.2, rfl⟩)

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ span A ↑(map ((TensorProduct.mk R A M) 1) p) ≤ baseChange A p
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
⊢ r = (r ^ m r * ∏ s ∈ S \ {r}, s ^ m s) * b

Tactic:
← hm

Goal state after:
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
⊢ r = a * b