mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r₁ r₂ : ι → R'
s : ι
hs : s ∈ S
H : ∑ x ∈ S, j (i (r₁ x) • v x) = ∑ x ∈ S, j (i (r₂ x) • v x)
⊢ r₁ s = r₂ s

Tactic:
← map_sum

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r₁ r₂ : ι → R'
s : ι
hs : s ∈ S
H : j (∑ x ∈ S, i (r₁ x) • v x) = j (∑ x ∈ S, i (r₂ x) • v x)
⊢ r₁ s = r₂ s
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
⊢ a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1 + 1) - 1

Tactic:
pow_add,

Goal state after:
case inr.inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
⊢ a ^ (c - b) * a ^ b - 1 = a ^ (c - b) * (a ^ b - 1 + 1) - 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
⊢ a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)

Tactic:
rw [← Nat.add_sub_assoc (one_le_pow (c - b) a ha0), ← mul_add_one, pow_add,
      Nat.sub_add_cancel (one_le_pow b a ha0)]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m > 0
hn : n > 0
⊢ k / m.gcd n ∣ c

Tactic:
rw [Nat.div_dvd_iff_dvd_mul hkm hm] at hmc

Goal state after:
case inr.inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k ∣ m * c
hnc : k / n ∣ c
hm : m > 0
hn : n > 0
⊢ k / m.gcd n ∣ c
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: ι : Type u_1
M : Type u_2
m n : ℕ
⊢ Fintype.card (Fin n → Fin m) = Fintype.card (Fin (m ^ n))

Tactic:
Fintype.card_fun,

Goal state after:
ι : Type u_1
M : Type u_2
m n : ℕ
⊢ Fintype.card (Fin m) ^ Fintype.card (Fin n) = Fintype.card (Fin (m ^ n))
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r' : ι → R'
s : ι
hs : s ∈ S
H : ∑ x ∈ S, j (i (r' x) • v x) = 0
⊢ r' s = 0

Tactic:
← map_sum

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r' : ι → R'
s : ι
hs : s ∈ S
H : j (∑ x ∈ S, i (r' x) • v x) = 0
⊢ r' s = 0
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ.zero
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n✝ : Fin (m + 1) → ℕ
f✝ : (i : Fin (m + 1)) → Fin (n✝ i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
fn : Fin 0
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * 0

Tactic:
exact isEmptyElim fn

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i

Tactic:
by
      induction m with
      | zero => simp
      | succ m ih =>
      rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]
      suffices
        ∀ (n : Fin m → ℕ) (nn : ℕ) (f : ∀ i : Fin m, Fin (n i)) (fn : Fin nn),
          ((∑ i : Fin m, ↑(f i) * ∏ j : Fin i, n (Fin.castLE i.prop.le j)) + ↑fn * ∏ j, n j) <
            (∏ i : Fin m, n i) * nn by
        solve_by_elim
      intro n nn f fn
      cases nn
      · exact isEmptyElim fn
      refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _ (Fin.is_le _)).trans_eq ?_
      rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
⊢ ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c

Tactic:
rw [this]

Goal state after:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
⊢ ((a % c + b % c) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: case isFalse.isTrue
n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : n ∣ x.natAbs
⊢ 0 = (x % ↑n).toNat

pp: case isFalse.isFalse
n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ n - x.natAbs % n = (x % ↑n).toNat

Tactic:
· rw [← Int.natCast_dvd] at h
      rw [Int.emod_eq_zero_of_dvd h, Int.toNat_zero]

Goal state after:
case isFalse.isFalse
n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ n - x.natAbs % n = (x % ↑n).toNat
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
v : ι → M
inst✝ : Unique ι
h : ∀ (l : ι →₀ R), v default = 0 → l default = 0
hv : v default = 0
⊢ False

Tactic:
simpa using h (.single default 1) hv

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case insert
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
this : x = Function.update x i 1 * Pi.mulSingle i (x i)
⊢ x ∈ H

Tactic:
rw [this]

Goal state after:
case insert
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
this : x = Function.update x i 1 * Pi.mulSingle i (x i)
⊢ Function.update x i 1 * Pi.mulSingle i (x i) ∈ H
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: P : Type u_4 → Prop
α : Type u_4
inst✝ : Finite α
hbase : ∀ (α : Type u_4) [Finite α] [Subsingleton α], P α
hstep : ∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α
n : ℕ
hn : Nat.card α = n
⊢ P α

Tactic:
induction n using Nat.strong_induction_on generalizing α with | _ n ih

Goal state after:
case h
P : Type u_4 → Prop
hbase : ∀ (α : Type u_4) [Finite α] [Subsingleton α], P α
hstep : ∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [Finite α], Nat.card α = m → P α
α : Type u_4
inst✝ : Finite α
hn : Nat.card α = n
⊢ P α
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝² : (i : η) → MulOneClass (f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H✝ : (i : η) → Submonoid (f i)
J : Submonoid ((i : η) → f i)
h : pi univ H✝ ≤ J
i : η
x✝¹ : (i : η) → f i
x✝ : x✝¹ ∈ map (MonoidHom.mulSingle f i) (H✝ i)
x : f i
hx : x ∈ ↑(H✝ i)
H : (MonoidHom.mulSingle f i) x = x✝¹
⊢ x✝¹ ∈ pi univ H✝

Tactic:
by simpa [← H]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ z * (c * d) = z * c * d

Tactic:
rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, sum, Finset.sum_mul, Finset.mul_sum, Finset.mul_sum,
          Finset.mul_sum]

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ i ∈ (b.repr c).support, z * ((b.repr c) i • b i * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a) =
    ∑ i ∈ (b.repr d).support, (∑ i ∈ (b.repr c).support, z * (b.repr c) i • b i) * (b.repr d) i • b i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

pp: case inr
α : Type u_1
s t : Set α
h : (s ∪ t).Infinite
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
· to_encard_tac
    rw [h.cast_ncard_eq, (h.subset subset_union_left).cast_ncard_eq,
      (h.subset subset_union_right).cast_ncard_eq]
    apply encard_union_le

Goal state after:
case inr
α : Type u_1
s t : Set α
h : (s ∪ t).Infinite
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: case inl
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
h✝ : Subsingleton R
⊢ Subsingleton (RingCon R) ↔ Subsingleton R

Tactic:
exact iff_of_true inferInstance ‹_›

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

Goal state before:
pp: case inr
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
h✝ : Nontrivial R
⊢ Nontrivial (RingCon R) ↔ Nontrivial R

Tactic:
exact iff_of_true inferInstance ‹_›

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
q : Submodule R M₂
x : M
y : M₂
⊢ (x, y) ∈ map (inr R M M₂) q ↔ (x, y) ∈ ⊥.prod q

Tactic:
simp [and_left_comm, eq_comm, and_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ f.range), u ∘ₛₗ f = v ∘ₛₗ f → u = v
h₁ : 0 ∘ₛₗ f = 0
⊢ ker 0 = ⊤

Tactic:
exact ker_zero

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this✝ : Fintype ι
this : x = ∑ i, x (Sum.inl i) • single (Sum.inl i) 1
⊢ x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)

Tactic:
rw [this]

Goal state after:
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this✝ : Fintype ι
this : x = ∑ i, x (Sum.inl i) • single (Sum.inl i) 1
⊢ ∑ i, x (Sum.inl i) • single (Sum.inl i) 1 ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Icc a b) (Icc (a + d) (b + d))

Tactic:
← Ici_inter_Iic,

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Ici a ∩ Iic b) (Icc (a + d) (b + d))
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case pos
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
⊢ ∏ k ∈ Ico m n, f k = ∏ x ∈ Ico m (n - m + m), f x

Tactic:
tsub_add_cancel_of_le h

Goal state after:
case pos
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
⊢ ∏ k ∈ Ico m n, f k = ∏ x ∈ Ico m n, f x
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
β : Type v
F : Type w
R : Type ?u.7
M : Type ?u.9
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m m' : M
a✝ b✝ : R
h : a✝ ∈ {r | r • m = r • m'}
h' : b✝ ∈ {r | r • m = r • m'}
⊢ a✝ + b✝ ∈ {r | r • m = r • m'}

Tactic:
by simpa [add_smul] using congr($h + $h')

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

Goal state before:
pp: α : Type u
a b : α
inst✝ : CommSemiring α
I : Ideal α
hab : a ∣ b
ha : a ∈ I
⊢ b ∈ I

Tactic:
obtain ⟨c, rfl⟩ := hab

Goal state after:
α : Type u
a : α
inst✝ : CommSemiring α
I : Ideal α
ha : a ∈ I
c : α
⊢ a * c ∈ I
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: case mp
α : Type u
inst✝ : Semiring α
y : α
I : Ideal α
b : α
hb : b ∈ I
a : α
hya : a * y ∈ span {y}
⊢ ∃ a_1, ∃ b_1 ∈ I, a_1 * y + b_1 = a * y + b

Tactic:
exact ⟨a, b, hb, rfl⟩

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

Goal state before:
pp: α : Type u
β : Type v
F : Type w
inst✝¹ : Semiring α
I : Ideal α
a b : α
inst✝ : Nontrivial α
⊢ Nontrivial (Ideal α)

Tactic:
by
  rcases @exists_maximal α _ _ with ⟨M, hM, _⟩
  exact nontrivial_of_ne M ⊤ hM

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x : α
⊢ span {x} = ⊤ ↔ IsUnit x

Tactic:
isUnit_iff_dvd_one,

Goal state after:
α : Type u
inst✝ : CommSemiring α
x : α
⊢ span {x} = ⊤ ↔ x ∣ 1
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ ∑ m ∈ range (n + 1), x ^ m * (-y) ^ (n - m) * ↑(n.choose m) =
    ∑ m ∈ range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
congr! 1 with m hm

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
⊢ x ^ m * (-y) ^ (n - m) * ↑(n.choose m) = (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
⊢ y ∈ I

Tactic:
by
      let J : Ideal α := Submodule.span α (insert x ↑I)
      have IJ : I ≤ J := Set.Subset.trans (subset_insert _ _) subset_span
      have xJ : x ∈ J := Ideal.subset_span (Set.mem_insert x I)
      obtain ⟨_, oJ⟩ := isMaximal_iff.1 H
      specialize oJ J x IJ hx xJ
      rcases Submodule.mem_span_insert.mp oJ with ⟨a, b, h, oe⟩
      obtain F : y * 1 = y * (a • x + b) := congr_arg (fun g : α => y * g) oe
      rw [← mul_one y, F, mul_add, mul_comm, smul_eq_mul, mul_assoc]
      refine Submodule.add_mem I (I.mul_mem_left a hxy) (Submodule.smul_mem I y ?_)
      rwa [Submodule.span_eq] at h

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x ∈ (LinearMap.toSpanSingleton R R e).ker ↔ x ∈ Ideal.span {1 - e}

Tactic:
Ideal.mem_span_singleton'

Goal state after:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x ∈ (LinearMap.toSpanSingleton R R e).ker ↔ ∃ a, a * (1 - e) = x
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)

Tactic:
eq_top_iff_one,

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : 1 ∈ span s
n : ℕ
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case single
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
i : ι
r : R i
⊢ Pi.single i r ∈ span (range fun i ↦ Pi.single i 1)

Tactic:
| single i r =>

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

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
x : R
hx : x ≠ 0
not_unit : ∀ (b : R), x * b ≠ 1
⊢ ∃ x, ∃ (_ : x ≠ 0), ∀ (b : R), x * b ≠ 1

Tactic:
exact ⟨x, hx, not_unit⟩

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
⊢ ⨆ i, map (lsingle i) (p i) ≤ submodule p

Tactic:
simp [iSup_le_iff, Submodule.map_le_iff_le_comap]

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: case mpr
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ (∃ u ∈ f, P u ∧ Q u) → (∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u

Tactic:
· rintro ⟨u, huf, hPu, hQu⟩
    exact ⟨⟨u, huf, hPu⟩, u, huf, hQu⟩

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: case right
α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
this : u = (u ∪ s) ∩ (u ∪ t)
⊢ p u

Tactic:
rw [this]

Goal state after:
case right
α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
this : u = (u ∪ s) ∩ (u ∪ t)
⊢ p ((u ∪ s) ∩ (u ∪ t))
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
⊢ map g (map f F) = F

Tactic:
by
  have : (g ∘ f) =ᶠ[𝓟 s] id := by simpa only [eventuallyEq_principal] using! hfg
  rw [map_map, map_congr (this.filter_mono hF), map_id]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ s ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ

Tactic:
rw [mem_kernMap, compl_surjective.exists]
  refine exists_congr (fun x ↦ and_congr_right fun _ ↦ ?_)
  rw [kernImage_compl, compl_eq_comm, eq_comm]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ ((∃ i, p i ∧ s i ⊆ t) ∧ ∃ i, p' i ∧ s' i ⊆ t) ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∪ s' i.snd ⊆ t

Tactic:
PProd.exists,

Goal state after:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ ((∃ i, p i ∧ s i ⊆ t) ∧ ∃ i, p' i ∧ s' i ⊆ t) ↔ ∃ a b, (p a ∧ p' b) ∧ s a ∪ s' b ⊆ t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
h : f = ⊥
⊢ map m f = ⊥

Tactic:
by simp only [h, map_bot]

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
P : α → Prop
⊢ (∃ᶠ (x : α) in f, P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x

Tactic:
by
  simp only [frequently_iff_forall_eventually_exists_and, @and_comm (P _),
    Set.ofPred_bijective.surjective.forall, Filter.Eventually, mem_ofPred]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
⊢ map m (f ⊓ g) = map m f ⊓ map m g

Tactic:
refine map_inf_le.antisymm ?_

Goal state after:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
⊢ map m f ⊓ map m g ≤ map m (f ⊓ g)
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case inr
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a b : α
hb : b ∈ Ioi a
⊢ atTop = comap Subtype.val atTop

Tactic:
← map_val_atTop_of_Ici_subset (Ici_subset_Ioi.2 hb),

Goal state after:
case inr
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a b : α
hb : b ∈ Ioi a
⊢ atTop = comap Subtype.val (map Subtype.val atTop)
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.FG ↔ ∃ n s, span R (range s) = N

Tactic:
by
  rw [fg_def]
  constructor
  · rintro ⟨S, Sfin, hS⟩
    obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding
    exact ⟨n, f, hS⟩
  · rintro ⟨n, s, hs⟩
    exact ⟨range s, finite_range s, hs⟩

Goal state after:
Module: Mathlib.Algebra.Module.Congruence.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : SMul R M
inst✝ : SMul S N
φ : R → S
f : M →ₑ[φ] N
r : R
x✝¹ x✝ : M
h : (Setoid.ker ⇑f) x✝¹ x✝
⊢ (Setoid.ker ⇑f) (r • x✝¹) (r • x✝)

Tactic:
Setoid.ker_def

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : SMul R M
inst✝ : SMul S N
φ : R → S
f : M →ₑ[φ] N
r : R
x✝¹ x✝ : M
h : f x✝¹ = f x✝
⊢ f (r • x✝¹) = f (r • x✝)
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ ∃ n, M' = N n

Tactic:
use S.attach.sup f

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ M' = N (S.attach.sup f)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : a < b
⊢ a - b ≤ c

Tactic:
simp [sub_eq_zero_of_lt h']

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: s : Set Ordinal.{u_3}
⊢ BddAbove ((fun x ↦ x + 1) '' s) ↔ BddAbove s

Tactic:
by
  constructor <;> rintro ⟨a, ha⟩
  · exact ⟨a, fun b hb ↦ (lt_add_one _).le.trans (ha (mem_image_of_mem _ hb))⟩
  · use a + 1
    simpa [upperBounds]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
⊢ (a * b + c) / (a * d) = b / d

Tactic:
obtain rfl | hd := eq_or_ne d 0

Goal state after:
case inl
a c : Ordinal.{u_4}
hc : c < a
b : Ordinal.{u_4}
⊢ (a * b + c) / (a * 0) = b / 0

case inr
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
⊢ (a * b + c) / (a * d) = b / d
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
⊢ o * ⨆ i, f i = ⨆ i, o * f i

Tactic:
by
  rw [← sSup_range, mul_sSup, ← Set.range_comp', sSup_range]

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inr.inl
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
c : ℕ
⊢ (b ^ k) ^ c ≤ n ↔ b ^ (c * k) ≤ n

Tactic:
Nat.pow_mul'

Goal state after:
case inr.inr.inl
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
c : ℕ
⊢ (b ^ k) ^ c ≤ n ↔ (b ^ k) ^ c ≤ n