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

Goal state before:
pp: case mp
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : DivisionSemiring S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
⊢ y ∈ x • p → x⁻¹ * y ∈ p

Tactic:
rintro ⟨a, ha : a ∈ p, rfl⟩

Goal state after:
case mp
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : DivisionSemiring S
inst✝ : Algebra R S
x : S
p : Submodule R S
hx : x ≠ 0
a : S
ha : a ∈ p
⊢ x⁻¹ * (DistribSMul.toLinearMap R S x) a ∈ p
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ span R s ^ 0 = span R (s ^ 0)

Tactic:
rw [pow_zero, pow_zero, one_eq_span_one_set]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
n : ℕ
x : A
hx : x ∈ M ^ n
⊢ C n x hx

Tactic:
by
  induction n generalizing x with
  | zero =>
    rw [pow_zero] at hx
    obtain ⟨r, rfl⟩ := mem_one.mp hx
    exact algebraMap r
  | succ n n_ih =>
    revert hx
    simp_rw [pow_succ']
    exact fun hx ↦ Submodule.mul_induction_on' (fun m hm x ih => mem_mul _ hm _ _ _ (n_ih ih))
      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ I.prod J = ⊤ ↔ I.prod J = ⊤.prod ⊤

Tactic:
prod_top_top

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ I.prod J = ⊤ ↔ I.prod J = ⊤
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I = ⊤
⊢ ¬(⊤.prod ⊤).IsPrime

Tactic:
prod_top_top,

Goal state after:
case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I = ⊤
⊢ ¬⊤.IsPrime
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α : Type u_6} [Fintype α],
    (∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)) →
      ∀ {M : Option α → Submodule R N} [∀ (i : Option α), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

Tactic:
intro _ _ ih _ _; rw [iSup_option]; infer_instance

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

Goal state before:
pp: case h.succ
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ m + 1
⊢ n ≤ m

Tactic:
exact Nat.succ_le_succ_iff.mp p

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

Goal state before:
pp: R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hr : r ∈ ↑(Ideal.span s)
hn : n ∈ N
⊢ r • n ∈ s • N

Tactic:
induction hr using Submodule.span_induction with

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

Goal state before:
pp: ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : r * (Pi.evalRingHom R i) x + y = 1
⊢ update 1 i y ∈ comap (Pi.evalRingHom R i) I

Tactic:
apply update_self i y 1 ▸ hy

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

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

Tactic:
by
    refine (eq_of_sub_eq_zero ?_).symm
    by_contra h
    have := mul_right_not_lt b h
    rw [sub_mul, mul_comm (_ / _), sub_eq_iff_eq_add'.2 (div_add_mod (a * b) b).symm] at this
    exact this (mod_lt _ hb)

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
e : S ≃+* T
⊢ Ideal.comap f (ker ↑e) = ker f

Tactic:
RingHom.ker_coe_equiv,

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
e : S ≃+* T
⊢ Ideal.comap f ⊥ = ker f
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : R
h : ∀ (m : M'), x • m = 0
⊢ ∀ (m : M), x • m = 0

Tactic:
exact fun m ↦ hf (by rw [map_smul, h, f.map_zero])

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
⊢ (image (fun x ↦ 1) s).gcd id = 1

Tactic:
image_const hs,

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
⊢ {1}.gcd id = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

Tactic:
← add_eq_one_iff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ I + J = 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
b : Associates α
⊢ ∀ (a_1 : α), a ∣ Associates.out ⟦a_1⟧ ↔ Associates.mk a ≤ ⟦a_1⟧

Tactic:
by
    simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
b : Associates α
⊢ ∀ (a_1 : α), Associates.out ⟦a_1⟧ ∣ a ↔ ⟦a_1⟧ ≤ Associates.mk a

Tactic:
by
    simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Subsingleton α
⊢ ∃ d, Associated (d ^ k) a

pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
⊢ ∃ d, Associated (d ^ k) a

Tactic:
· use 0
    rw [Subsingleton.elim a (0 ^ k)]

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
⊢ ∃ d, Associated (d ^ k) a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
h : ¬gcd x y = 0
x' : α
ex : x = gcd x y * x'
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')

Tactic:
obtain ⟨y', ey⟩ := gcd_dvd_right x y

Goal state after:
case neg
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
h : ¬gcd x y = 0
x' : α
ex : x = gcd x y * x'
y' : α
ey : y = gcd x y * y'
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : lcm a b = 0
this : Associated (a * b) 0
⊢ a = 0 ∨ b = 0

Tactic:
← mul_eq_zero,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : lcm a b = 0
this : Associated (a * b) 0
⊢ a * b = 0
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
⊢ Nontrivial R

Tactic:
by
  by_contra! h
  exact zero_ne_one (eq_of_fin_equiv R <| .ofSubsingleton ..)

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

Goal state before:
pp: case a
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ #κ ≤ #ι

Tactic:
exact linearIndependent_le_basis b v i

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

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∈ s
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
obtain ⟨t, hat, rfl⟩ : ∃ t, a ∉ t ∧ insert a t = s :=
        ⟨s.erase a, Finset.notMem_erase a s, Finset.insert_erase has⟩
      by_cases hbt : b ∈ t
      · obtain ⟨u, hbu, rfl⟩ : ∃ u, b ∉ u ∧ insert b u = t :=
          ⟨t.erase b, Finset.notMem_erase b t, Finset.insert_erase hbt⟩
        have hp' : ∀ i ∈ u, IsPrime (f i) := by
          intro i hiu
          refine hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_ <;>
              rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Finset.coe_insert, Set.biUnion_insert, Set.biUnion_insert, ←
          Set.union_assoc, subset_union_prime' hp'] at h
        rwa [Finset.exists_mem_insert, Finset.exists_mem_insert]
      · have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f a : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]

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

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
i' : l
j' : m
hi : f.symm i ≠ i'
⊢ single i j r (f i') (g j') = single (f.symm i) (g.symm j) r i' j'

Tactic:
rw [single_apply_of_row_ne hi, single_apply_of_row_ne]

Goal state after:
case inl.hi
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
i' : l
j' : m
hi : f.symm i ≠ i'
⊢ i ≠ f i'
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_10
n : Type u_11
R : Type u_12
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : MulOne R
inst✝¹ : AddCommMonoid R
inst✝ : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ (A * B).submatrix ⇑e.symm ⇑e.symm = 1 ↔ B * A = 1

Tactic:
← submatrix_mul_equiv _ _ _ (.refl _),

Goal state after:
m : Type u_10
n : Type u_11
R : Type u_12
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : MulOne R
inst✝¹ : AddCommMonoid R
inst✝ : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ A.submatrix ⇑e.symm ⇑(Equiv.refl n) * B.submatrix ⇑(Equiv.refl n) ⇑e.symm = 1 ↔ B * A = 1
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: case mp
α : 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 β
x : ↑T
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf T hT x ∈ t → ∃ i x_1, f i x_1 ∈ t ∧ inclusion ⋯ x_1 = inclusion hT x

Tactic:
refine fun h => ⟨i, ⟨x, hi⟩, ?_, rfl⟩

Goal state after:
case mp
α : 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 β
x : ↑T
i : ι
hi : ↑x ∈ S i
h : iUnionLift S f hf T hT x ∈ t
⊢ f i ⟨↑x, hi⟩ ∈ t
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ ((fun s ↦ { support := s.toFinset, toFun := fun a ↦ count a s, mem_support_toFun := ⋯ })
        ((fun f ↦ Finsupp.toMultiset f) f))
      a =
    f a

Tactic:
by
      simp only [Finsupp.toMultiset_apply, Finsupp.sum, Multiset.count_sum',
        Multiset.count_singleton, mul_boole, Finsupp.coe_mk, Finsupp.mem_support_iff,
        Multiset.count_nsmul, Finset.sum_ite_eq, ite_not, ite_eq_right_iff]
      exact Eq.symm

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
⊢ ∀ (a : α →₀ ℕ), (a.sum fun x ↦ id) = n ↔ ∑ i, Finsupp.equivFunOnFinite a i = n

Tactic:
by simp [Finsupp.sum_fintype]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
let s : TwoSidedIdeal R := .mk'
      {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}
      ⟨0, ⟨zero_mem _, ⟨0, ⟨zero_mem _, zero_add _⟩⟩⟩⟩
      (by rintro _ _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩ ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩;
          exact ⟨x + a, ⟨add_mem _ hx ha, ⟨y + b, ⟨add_mem _ hy hb, by abel⟩⟩⟩⟩)
      (by rintro _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨-x, ⟨neg_mem _ hx, ⟨-y, ⟨neg_mem _ hy, by abel⟩⟩⟩⟩)
      (by rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨_, ⟨mul_mem_left _ _ _ hx, ⟨_, ⟨mul_mem_left _ _ _ hy, mul_add _ _ _ |>.symm⟩⟩⟩⟩)
      (by rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨_, ⟨mul_mem_right _ _ _ hx, ⟨_, ⟨mul_mem_right _ _ _ hy, add_mul _ _ _ |>.symm⟩⟩⟩⟩)
    suffices (I.ringCon ⊔ J.ringCon) ≤ s.ringCon by
      intro h; convert! this h; rw [rel_iff, sub_zero, mem_mk']; rfl
    refine sup_le (fun x y h => ?_) (fun x y h => ?_) <;> rw [rel_iff] at h ⊢ <;> rw [mem_mk']
    exacts [⟨_, ⟨h, ⟨0, ⟨zero_mem _, add_zero _⟩⟩⟩⟩, ⟨0, ⟨zero_mem _, ⟨_, ⟨h, zero_add _⟩⟩⟩⟩]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (⨅ i, I i).ringCon = ⨅ i, (I i).ringCon

Tactic:
by
  simp only [iInf, sInf_ringCon]; congr!; ext; simp

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
ι : Sort u_1
S : ι → Subalgebra R A
motive : (x : A) → x ∈ ⨆ i, S i → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯
add : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r) ⋯
⊢ motive x mem

Tactic:
refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, S i) (hc : motive x hx) ↦ hc
  exact iSup_induction S (motive := fun x' ↦ ∃ h, motive x' h) mem
    (fun _ _ h ↦ ⟨_, basic _ _ h⟩) (fun _ _ h h' ↦ ⟨_, add _ _ _ _ h.2 h'.2⟩)
    (fun _ _ h h' ↦ ⟨_, mul _ _ _ _ h.2 h'.2⟩) fun _ ↦ ⟨_, algebraMap _⟩

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
⊢ ∀ (a : Subalgebra R R), a = default

Tactic:
by
      intro S
      refine le_antisymm ?_ bot_le
      intro _ _
      simp only [Set.mem_range, mem_bot, algebraMap_self_apply, exists_apply_eq_apply, default]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Surjective ⇑f
S : Subalgebra R B
⊢ S ≤ f.range

Tactic:
simp [(AlgHom.range_eq_top f).2 hf]

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

Goal state before:
pp: case add
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : x ∈ adjoin R s), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : x ∈ adjoin R s), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (r • y) hx ⋯
x y : A
hx : x ∈ adjoin R s
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ + y✝) hx ⋯

Tactic:
exact add_right _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: case add
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : A
hx : x ∈ adjoin R s
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ + y✝) hx ⋯

Tactic:
exact add_right _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ r • (b * c * a) = r • (b * (c * a))

Tactic:
ha.right_assoc

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ r • (b * (c * a)) = r • (b * (c * a))
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ x ∈ adjoin R (↑S ∪ ⇑f ⁻¹' {0})

Tactic:
← add_sub_cancel y x

Goal state after:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ y + (x - y) ∈ adjoin R (↑S ∪ ⇑f ⁻¹' {0})
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
p : ι →₀ M
n : N
⊢ (finsuppLeft R S M N ι) (p ⊗ₜ[R] n) = p.sum fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n)

Tactic:
induction p using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [add_tmul, map_add, hf, hg, Finsupp.sum_add_index]
  | single => simp [finsuppLeft]

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
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ⇑f
⊢ ∃ h, f ∘ₗ h = LinearMap.id

Tactic:
by
    classical
      choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf
      replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ DFunLike.congr_fun (hg i)
      refine ⟨DFinsupp.coprodMap g, ?_⟩
      ext i x j
      simp only [comp_apply, id_apply, DFinsupp.lsingle_apply, DFinsupp.coprodMap_apply_single, hg]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
t : (ι →₀ M) ⊗[R] N
i : ι
⊢ ((finsuppLeft R S M N ι) t) i = (rTensor N (Finsupp.lapply i)) t

Tactic:
by
  induction t with
  | zero => simp
  | tmul f n => simp only [finsuppLeft_apply_tmul_apply, rTensor_tmul, Finsupp.lapply_apply]
  | add x y hx hy => simp [map_add, hx, hy]

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 ι
p : ι →₀ R
n : N
i : ι
⊢ ((finsuppScalarLeft R N ι) (p ⊗ₜ[R] n)) i = (p.sum fun i m ↦ Finsupp.single i (m • n)) i

Tactic:
finsuppScalarLeft_apply_tmul_apply,

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
p : ι →₀ R
n : N
i : ι
⊢ p i • n = (p.sum fun i m ↦ Finsupp.single i (m • n)) i