mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
x y : α
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I

Tactic:
by_contra! rid
    have hx := maximally_disjoint (I ⊔ span {x}) (Submodule.lt_sup_iff_notMem.mpr rid.1)
    have hy := maximally_disjoint (I ⊔ span {y}) (Submodule.lt_sup_iff_notMem.mpr rid.2)
    simp only [Set.not_disjoint_iff, SetLike.mem_coe, Submodule.mem_sup,
      mem_span_singleton] at hx hy
    obtain ⟨s₁, ⟨i₁, hi₁, ⟨_, ⟨r₁, rfl⟩, hr₁⟩⟩, hs₁⟩ := hx
    obtain ⟨s₂, ⟨i₂, hi₂, ⟨_, ⟨r₂, rfl⟩, hr₂⟩⟩, hs₂⟩ := hy
    refine disjoint.ne_of_mem
      (I.add_mem (I.mul_mem_left (i₁ + x * r₁) hi₂) <| I.add_mem (I.mul_mem_right (y * r₂) hi₁) <|
        I.mul_mem_right (r₁ * r₂) hxy)
      (S.mul_mem hs₁ hs₂) ?_
    rw [← hr₁, ← hr₂]
    ring

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ x.powerset
⊢ #y ∈ range (#x + 1)

Tactic:
rw [mem_range, Nat.lt_succ_iff]

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ x.powerset
⊢ #y ≤ #x
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
this : (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset

Tactic:
this,

Goal state after:
case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
this : (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)
⊢ a ^ c * s.sum ^ (s.card * n + 1 + (n - c)) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
not_field : ¬IsField R
max : ⊥.IsMaximal
⊢ False

Tactic:
obtain ⟨I, hIbot, hItop⟩ := not_isField_iff_exists_ideal_bot_lt_and_lt_top.mp not_field

Goal state after:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
not_field : ¬IsField R
max : ⊥.IsMaximal
I : Ideal R
hIbot : ⊥ < I
hItop : I < ⊤
⊢ False
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : 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
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
s t : Set α
hqs : q s
hqt : q t
⊢ q (s ∩ t)

Tactic:
by
    let 𝓕 : Filter α :=
    { sets := {s | ∀ t, q t → q (s ∩ t)}
      univ_sets := by simp
      sets_of_superset ha hab t ht := q_mono (inter_subset_inter_left _ hab) (ha t ht)
      inter_sets ha hb t ht := by simpa [inter_assoc] using ha _ (hb _ ht) }
    exact (le_iInf_iff.mpr A : 𝓕 ≤ iInf f) hqs.1 _ hqt

Goal state after:
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : min x₂ y₂ ≤ max x₁ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂

Tactic:
min_eq_left (le_of_lt h2.2),

Goal state after:
α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ max x₁ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
c : β → α
h : range c ∈ f
W : Set β
W_in : W ∈ comap c f
⊢ c '' W ∈ map c (comap c f)

Tactic:
exact image_mem_map W_in

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ sᶜ ∈ 𝓟 t ↔ t ⊆ sᶜ

Tactic:
mem_principal

Goal state after:
α : Type u_1
s t : Set α
⊢ t ⊆ sᶜ ↔ t ⊆ sᶜ
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s s✝ : Set α
⊢ s✝ ∈ ⨆ i, f i ⊓ 𝓟 s ↔ s✝ ∈ (⨆ i, f i) ⊓ 𝓟 s

Tactic:
simp only [mem_iSup, mem_inf_principal]

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

Goal state before:
pp: α : Type u
s : Set α
f : Filter α
⊢ (∀ x ∈ f, x ∈ 𝓟 s) ↔ ∀ V ∈ f, s ⊆ V

Tactic:
mem_principal

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn m s
F : Filter α
hF : F ∈ Iic (𝓟 s)
G : Filter α
hG : G ∈ Iic (𝓟 s)
⊢ map m F = map m G → F = G

Tactic:
simp [map_eq_map_iff_of_injOn (le_principal_iff.mp hF) (le_principal_iff.mp hG) hm]

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

Goal state before:
pp: k a : ℕ
h : k ≤ a
⊢ a ≤ a - k + k

Tactic:
Nat.sub_add_cancel h

Goal state after:
k a : ℕ
h : k ≤ a
⊢ a ≤ a
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this✝ : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : Ordinal.liftPrincipalSeg.toRelEmbedding o = c.ord
this : lift.{u + 1, u} o.card = c
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
exact ⟨_, this.symm⟩

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

Goal state before:
pp: a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
⊢ IsSuccLimit (a - b)

Tactic:
by
  rw [isSuccLimit_iff, Ordinal.sub_ne_zero_iff_lt, isSuccPrelimit_iff_succ_lt]
  refine ⟨h, fun c hc ↦ ?_⟩
  rw [lt_sub] at hc ⊢
  rw [succ_eq_add_one, ← add_assoc]
  exact ha.succ_lt hc

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

Goal state before:
pp: case pos
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
⊢ ⨆ i, f i + 1 ≤ ⨆ i, f i

pp: case neg
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : ¬BddAbove (range f)
⊢ ⨆ i, f i + 1 ≤ ⨆ i, f i

Tactic:
· rw [ciSup_le_iff' (bddAbove_range_add_one_iff.2 hf')]
    intro i
    obtain ⟨j, hj⟩ := exists_gt i
    apply (le_ciSup hf' j).trans'
    rw [add_one_le_iff]
    exact hf hj

Goal state after:
case neg
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : ¬BddAbove (range f)
⊢ ⨆ i, f i + 1 ≤ ⨆ i, f i
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ∀ {a b : Ordinal.{u}}, a + 1 ≤ b ↔ a < b

Tactic:
exact succ_le_iff'

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

Goal state before:
pp: ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ lsub (familyOfBFamily' r ho f) = lsub (familyOfBFamily' r' ho' f)

Tactic:
lsub_eq_blsub',

Goal state after:
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ o.blsub f = lsub (familyOfBFamily' r' ho' f)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
⊢ log b y < x ↔ y < b ^ x

Tactic:
by
  rcases log.go_spec hb hy (Nat.lt_pow_self hb) with ⟨-, H₁, H₂⟩
  rw [log, if_neg (Nat.not_le_of_lt hb)]
  cases Nat.lt_or_ge (log.go y b y).snd x with
  | inl h =>
    exact iff_of_true h <| Nat.lt_of_lt_of_le H₂ <| Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) h
  | inr h =>
    refine iff_of_false (Nat.not_lt_of_ge h) <| Nat.not_lt_of_ge <| Nat.le_trans ?_ H₁
    exact Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) h

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

Goal state before:
pp: a b c : Ordinal.{u_1}
b0 : b ≠ 0
h : IsSuccLimit c
⊢ a < b ^ c ↔ ∃ c' < c, a < b ^ c'

Tactic:
simpa using (opow_le_of_isSuccLimit b0 h).not

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

Goal state before:
pp: a b c : Ordinal.{u_4}
h : c ∣ b
⊢ a % b % c = a % c

Tactic:
by
  nth_rw 2 [← div_add_mod a b]
  rcases h with ⟨d, rfl⟩
  rw [mul_assoc, mul_add_mod_self]

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

Goal state before:
pp: case inr.inr.add_one
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ (b + (c + 1)) = a ^ b * a ^ (c + 1)

Tactic:
rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]

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

Goal state before:
pp: b x y : ℕ
h : x ≤ b ^ y
⊢ clog b x ≤ y

Tactic:
rcases Nat.lt_or_ge 1 b with hb | hb
  · rwa [clog_le_iff_le_pow hb]
  · grind [clog_of_left_le_one]

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

Goal state before:
pp: b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ n ≤ b ^ clog c n

Tactic:
calc
    n ≤ c ^ clog c n := le_pow_clog hc _
    _ ≤ b ^ clog c n := Nat.pow_le_pow_left hb _

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

Goal state before:
pp: b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
⊢ c ≤ log b x

Tactic:
obtain rfl | hx := eq_or_ne x 0
  · rw [nonpos_iff_eq_zero, opow_eq_zero] at h
    exact (zero_lt_one.asymm <| h.1 ▸ hb).elim
  · exact (opow_le_iff_le_log hb hx).1 h

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

Goal state before:
pp: o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
⊢ ¬IsPrincipal op o ↔ ∃ a < o, o ≤ op a a

Tactic:
by
  simp [isPrincipal_iff_of_monotone h₁ h₂]

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a + b ≤ b ↔ a + b = b

Tactic:
exact (isNormal_add_right a).strictMono.le_apply.ge_iff_eq'

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

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
⊢ ¬BddAbove {o | IsPrincipal op o}

Tactic:
rintro ⟨a, ha⟩
  exact ((le_nfp _ _).trans (ha (isPrincipal_nfp_iSup op (succ a)))).not_gt (lt_succ a)

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ o)

Tactic:
isPrincipal_add_iff_add_self_lt

Goal state after:
case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ ∀ b < ω ^ o, b + b < ω ^ o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
⊢ Ordinal.lift.{v, u} (ω_ o) = ω_ (Ordinal.lift.{v, u} o)

Tactic:
simp [omega_eq_preOmega]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case isSuccPrelimit
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
x : Cardinal.{max u_1 v}
⊢ (x ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)) ↔ x ∈ range fun a ↦ preBeth ↑a

Tactic:
constructor <;> rintro ⟨⟨i, hi⟩, rfl⟩

Goal state after:
case isSuccPrelimit.mp
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi : i ∈ Iio o
⊢ (fun i ↦ lift.{v, u_1} (preBeth ↑i)) ⟨i, hi⟩ ∈ range fun a ↦ preBeth ↑a

case isSuccPrelimit.mpr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{max u_1 v}
hi : i ∈ Iio (Ordinal.lift.{v, u_1} o)
⊢ (fun a ↦ preBeth ↑a) ⟨i, hi⟩ ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1
a b : Cardinal.{u_1}
h : a * b = a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

pp: case refine_2
a b : Cardinal.{u_1}
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 → a * b = a

Tactic:
· rcases le_or_gt ℵ₀ a with ha | ha
    · have : a ≠ 0 := by
        rintro rfl
        exact ha.not_gt aleph0_pos
      left
      rw [and_assoc]
      use ha
      constructor
      · rw [← not_lt]
        exact fun hb => ne_of_gt (hb.trans_le (le_mul_left this)) h
      · rintro rfl
        apply this
        rw [mul_zero] at h
        exact h.symm
    right
    by_cases h2a : a = 0
    · exact Or.inr h2a
    have hb : b ≠ 0 := by
      rintro rfl
      apply h2a
      rw [mul_zero] at h
      exact h.symm
    left
    rw [← h, mul_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
    rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)
    · contradiction
    · contradiction
    rw [← Ne] at h2a
    rw [← Cardinal.one_le_iff_ne_zero] at h2a hb
    norm_cast at h2a hb h ⊢
    apply le_antisymm _ hb
    rw [← not_lt]
    apply fun h2b => ne_of_gt _ h
    conv_rhs => left; rw [← mul_one n]
    rw [Nat.mul_lt_mul_left]
    · exact id
    apply Nat.lt_of_succ_le h2a

Goal state after:
case refine_2
a b : Cardinal.{u_1}
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 → a * b = a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c ≤ ℵ_ 1 ↔ c ≤ ℵ_ 1

Tactic:
by
  simpa using lift_le (b := ℵ₁)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case add_one
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
a✝ : a + 1 = a → (a + 1).cof ≤ (f (a + 1)).cof
⊢ (a + 1).cof ≤ (f (a + 1)).cof

Tactic:
cof_add_one,

Goal state after:
case add_one
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
a✝ : a + 1 = a → (a + 1).cof ≤ (f (a + 1)).cof
⊢ 1 ≤ (f (a + 1)).cof
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #↑s ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ (⨆ a, ↑a).card ≤ c

Tactic:
apply card_iSup_le_lift

Goal state after:
case hι
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #↑s ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ Cardinal.lift.{u, u + 1} #↑s ≤ Cardinal.lift.{u + 1, u} c

case hf
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #↑s ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ ∀ (i : ↑s), (↑i).card ≤ c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.inl
a c : Ordinal.{u_1}
hb : succ c ≠ 0
⊢ (a + c + 1).cof = (c + 1).cof

Tactic:
cof_add_one,

Goal state after:
case inr.inl
a c : Ordinal.{u_1}
hb : succ c ≠ 0
⊢ 1 = (c + 1).cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a : Cardinal.{u}
ha : a ≤ ℵ₀
b : ℕ
⊢ a ^ ↑b ≤ ℵ₀

Tactic:
simpa [ha] using power_nat_le_max (c := a)

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h.cons.inl
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : f i = 0
⊢ p (single i (f i) + erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })

Tactic:
rw [h, single_zero, zero_add]

Goal state after:
case h.cons.inl
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : f i = 0
⊢ p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
⊢ (finChoice q).eval = q

Tactic:
refine induction_on_fintype_pi q (fun a ↦ ?_)

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ (finChoice fun x ↦ ⟦a x⟧).eval = fun x ↦ ⟦a x⟧
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a : Fin (n + 2) → α
⊢ prod a = (∏ i, a i.castSucc) * a (Fin.last (n + 1))

Tactic:
prod,

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a : Fin (n + 2) → α
⊢ (prod fun i ↦ a i.castSucc) * a (Fin.last (n + 1)) = (∏ i, a i.castSucc) * a (Fin.last (n + 1))
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝⁴² : Semiring R
inst✝⁴¹ : Semiring R₂
inst✝⁴⁰ : Semiring S
inst✝³⁹ : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝³⁸ : AddCommMonoid M
inst✝³⁷ : AddCommMonoid M₂
inst✝³⁶ : AddCommMonoid N
inst✝³⁵ : AddCommMonoid N₂
inst✝³⁴ : AddCommMonoid P
inst✝³³ : AddCommMonoid P₂
inst✝³² : AddCommMonoid Pₗ
inst✝³¹ : Module R M
inst✝³⁰ : Module R M₂
inst✝²⁹ : Module S N
inst✝²⁸ : Module S N₂
inst✝²⁷ : Module R₂ P
inst✝²⁶ : Module S₂ P
inst✝²⁵ : Module R P₂
inst✝²⁴ : Module S₂ P₂
inst✝²³ : Module R Pₗ
inst✝²² : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝²¹ : AddCommGroup M'
inst✝²⁰ : AddCommGroup P'
inst✝¹⁹ : Module R M'
inst✝¹⁸ : Module R₂ P'
inst✝¹⁷ : Module S₂ P'
inst✝¹⁶ : SMulCommClass S₂ R₂ P
inst✝¹⁵ : SMulCommClass S R Pₗ
inst✝¹⁴ : SMulCommClass S₂ R₂ P'
inst✝¹³ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
R' : Type u_14
S' : Type u_15
inst✝¹² : Semiring R'
inst✝¹¹ : Semiring S'
inst✝¹⁰ : Module R' M
inst✝⁹ : Module S' N
inst✝⁸ : Module R' Pₗ
inst✝⁷ : Module S' Pₗ
inst✝⁶ : SMulCommClass S' R' Pₗ
inst✝⁵ : SMul S' S
inst✝⁴ : IsScalarTower S' S N
inst✝³ : IsScalarTower S' S Pₗ
inst✝² : SMul R' R
inst✝¹ : IsScalarTower R' R M
inst✝ : IsScalarTower R' R Pₗ
B : M →ₗ[R] N →ₗ[S] Pₗ
r' : R'
m : M
x✝ : N
⊢ (B (r' • m)) x✝ = r' • (B m) x✝

Tactic:
by
      rw [← smul_one_smul R r' m, map_smul₂, smul_one_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring S
inst✝¹² : SMul S R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : Module S M
inst✝⁶ : Module S P
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S R P
inst✝³ : AddCommMonoid M'
inst✝² : Module S M'
inst✝¹ : AddCommMonoid P'
inst✝ : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective ⇑k
f : M →ₗ[R] P
hf : ∀ (m : M'), f (i m) ∈ k.range
m : M'
this : k ((i.restrictScalarsRange k hk f hf) m) = (k ∘ₗ (↑S f ∘ₗ i).codLift k hk hf) m
⊢ k ((i.restrictScalarsRange k hk f hf) m) = f (i m)

Tactic:
this,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring S
inst✝¹² : SMul S R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : Module S M
inst✝⁶ : Module S P
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S R P
inst✝³ : AddCommMonoid M'
inst✝² : Module S M'
inst✝¹ : AddCommMonoid P'
inst✝ : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective ⇑k
f : M →ₗ[R] P
hf : ∀ (m : M'), f (i m) ∈ k.range
m : M'
this : k ((i.restrictScalarsRange k hk f hf) m) = (k ∘ₗ (↑S f ∘ₗ i).codLift k hk hf) m
⊢ (k ∘ₗ (↑S f ∘ₗ i).codLift k hk hf) m = f (i m)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
hv0 : ∑ i ∈ s, v i = 0
i : ι
hi : i ∈ s
⊢ v i ∈ ⨆ j, ⨆ (_ : j ≠ i), p j

Tactic:
← s.add_sum_erase _ hi,

Goal state after:
case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
i : ι
hv0 : v i + ∑ x ∈ s.erase i, v x = 0
hi : i ∈ s
⊢ v i ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case left
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ (a * d) • s = (b * c) • s

Tactic:
calc (a * d) • s
        = d • a • s := by rw [mul_comm, mul_smul]
      _ = -(d • c • t) := by rw [eq_neg_iff_add_eq_zero, ← smul_add, h₁, smul_zero]
      _ = (b * c) • s := ?_

Goal state after:
case left
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ -(d • c • t) = (b * c) • s
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x✝ : X
⊢ ((smulAddHom ℤ (FreeAbelianGroup X)) 1) (of x✝) = (AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)

Tactic:
smulAddHom_apply,

Goal state after:
X : Type u_1
x✝ : X
⊢ 1 • of x✝ = (AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
⊢ toFreeAbelianGroup.comp toFinsupp = AddMonoidHom.id (FreeAbelianGroup X)

Tactic:
by
  ext
  rw [toFreeAbelianGroup, toFinsupp, AddMonoidHom.comp_apply, lift_apply_of,
    liftAddHom_apply_single, AddMonoidHom.flip_apply, smulAddHom_apply, one_smul,
    AddMonoidHom.id_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case a
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
⊢ LinearIndepOn R id (⋃ a, range fun b ↦ f ⟨a, b⟩.fst ⟨a, b⟩.snd)

Tactic:
apply linearIndepOn_id_iUnion_finite (fun j => (hindep j).linearIndepOn_id) hd

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝² : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ ↑(image₂ f (s ∩ s') (t ∪ t')) ⊆ ↑(image₂ f s t ∪ image₂ f s' t')

Tactic:
by
    push_cast
    exact Set.image2_inter_union_subset_union

Goal state after: