mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case succ
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
⊢ (if h : ↑i + ↑i + 1 < n + 1 + 1 then v ⟨↑i + ↑i + 1, ⋯⟩ else v ⟨↑i + ↑i + 1 - (n + 1 + 1), ⋯⟩) = v (i + i + 1)

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ↑i + ↑i + 1 < n + 1 + 1
⊢ v ⟨↑i + ↑i + 1, ⋯⟩ = v (i + i + 1)

case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬↑i + ↑i + 1 < n + 1 + 1
⊢ v ⟨↑i + ↑i + 1 - (n + 1 + 1), ⋯⟩ = v (i + i + 1)
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
⊢ ↑(a - 1) = if a = 0 then n✝ + 1 else ↑a - 1

Tactic:
split_ifs with h

Goal state after:
case pos
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : a = 0
⊢ ↑(a - 1) = n✝ + 1

case neg
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : ¬a = 0
⊢ ↑(a - 1) = ↑a - 1
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
p : Submodule R M
h : ∀ (i : ι), b i ∈ p
⊢ range ⇑b ⊆ ↑p

Tactic:
rintro - ⟨i, rfl⟩

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
p : Submodule R M
h : ∀ (i : ι), b i ∈ p
i : ι
⊢ b i ∈ ↑p
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a : G
⊢ a ≡ 0 [PMOD p] ↔ ∃ z, a = z • p

Tactic:
rw [modEq_comm, modEq_iff_eq_add_zsmul]
  simp_rw [zero_add]

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

Goal state before:
pp: case succ
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1, (-1) ^ ↑n_1 = if Even n then 0 else 1
⊢ (if Even n then 0 else 1) + (-1) ^ n = if Even n then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1, (-1) ^ ↑n_1 = if Even n then 0 else 1
h : Even n
⊢ 0 + (-1) ^ n = 1

case neg
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1, (-1) ^ ↑n_1 = if Even n then 0 else 1
h : ¬Even n
⊢ 1 + (-1) ^ n = 0
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2.inl
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun x1 x2 ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)

Tactic:
rw [succAbove_of_castSucc_lt, contractNth_apply_of_lt _ _ _ _ h,
        succAbove_of_castSucc_lt]

Goal state after:
case refine_2.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ i.castSucc < a

case refine_2.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ i.castSucc.castSucc < a.succ
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2.inr.inr
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ partialProd g i.castSucc.succ * a.contractNth (fun x1 x2 ↦ x1 * x2) g i = partialProd g i.succ.castSucc * g i.succ

pp: case refine_2.inr.inr.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ a ≤ i.castSucc

pp: case refine_2.inr.inr.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ a.succ ≤ i.castSucc.castSucc

Tactic:
contractNth_apply_of_gt _ _ _ _ h,

Goal state after:
case refine_2.inr.inr
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ partialProd g i.castSucc.succ * g i.succ = partialProd g i.succ.castSucc * g i.succ

case refine_2.inr.inr.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ a ≤ i.castSucc

case refine_2.inr.inr.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ a.succ ≤ i.castSucc.castSucc
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
h : a ≤ b
⊢ a ≡ b [MOD n] ↔ n ∣ b - a

Tactic:
by
  rw [modEq_iff_dvd, ← Int.natCast_dvd_natCast, Int.ofNat_sub h]

Goal state after:
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 : LinearIndependent R v
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
⊢ LinearIndependent R' (⇑j ∘ v)

Tactic:
rw [linearIndependent_iff'] at hv ⊢

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 ι) (g : ι → R'), ∑ i ∈ s, g i • (⇑j ∘ v) i = 0 → ∀ i ∈ s, g i = 0
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 ι) (g : ι → R'), ∑ i ∈ s, g i • (⇑j ∘ v) i = 0 → ∀ i ∈ s, g i = 0

Tactic:
intro S r' H s hs

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'
H : ∑ i ∈ S, r' i • (⇑j ∘ v) i = 0
s : ι
hs : s ∈ S
⊢ r' s = 0
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 % c + b % c) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c

Tactic:
split_ifs with h

Goal state after:
case pos
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
⊢ (a % c + b % c) % c + c = a % c + b % c

case neg
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : ¬c ≤ a % c + b % c
⊢ (a % c + b % c) % c + 0 = a % c + b % c
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
a b c : Fin n
⊢ (a + b) * c = a * c + b * c

Tactic:
by
    rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Nonempty α
inst✝ : Subsingleton α
⊢ Nat.card α = 1

Tactic:
simp [card_eq_one_iff_unique, *]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type u_1
v : ι → M
s : Set ι
hs : LinearIndepOn R v s
⊢ s.encard ≤ toENat (Module.rank R M)

Tactic:
by
  simpa using OrderHom.mono (β := ℕ∞) Cardinal.toENat hs.linearIndependent.cardinal_lift_le_rank

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
le : ∀ (s : Finset M), s.card = n → ¬LinearIndepOn R id ↑s
⊢ Module.rank R M < ↑n

Tactic:
obtain _ | n := n

Goal state after:
case zero
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
le : ∀ (s : Finset M), s.card = 0 → ¬LinearIndepOn R id ↑s
⊢ Module.rank R M < ↑0

case succ
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
le : ∀ (s : Finset M), s.card = n + 1 → ¬LinearIndepOn R id ↑s
⊢ Module.rank R M < ↑(n + 1)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case h.refine_1
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
⊢ (if x = a then b else f₀ x) ∈ t

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
h : x = a
⊢ b ∈ t

case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
h : ¬x = a
⊢ f₀ x ∈ t
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : 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
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
j : η
hj : j ∈ I
this : j ≠ i
⊢ Pi.mulSingle j (x j) ∈ H

Tactic:
exact h2 _ (Finset.mem_insert_of_mem hj)

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ ¬s.Infinite

Tactic:
Set.Infinite,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ ¬¬s.Finite
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : ↥(span R (range ⇑b))
i : ι
⊢ (algebraMap R S) (((restrictScalars R b).repr m) i) = (b.repr ↑m) i

Tactic:
by
  suffices
    Finsupp.mapRange.linearMap (Algebra.linearMap R S) ∘ₗ (b.restrictScalars R).repr.toLinearMap =
      ((b.repr : M →ₗ[S] ι →₀ S).restrictScalars R).domRestrict _
    by exact DFunLike.congr_fun (LinearMap.congr_fun this m) i
  refine Basis.ext (b.restrictScalars R) fun _ => ?_
  simp only [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply, map_one,
    Basis.repr_self, Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single,
    Algebra.linearMap_apply, LinearMap.domRestrict_apply,
    Basis.restrictScalars_apply, LinearMap.coe_restrictScalars]

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

Goal state before:
pp: α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Tactic:
classical
  have hu := finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm
  rw [ncard_eq_toFinset_card _ hu,
    Finite.toFinset_union (hu.subset subset_union_left)
      (hu.subset subset_union_right)] at hst
  obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst
  exact ⟨r', by simpa, by simpa using hr'⟩

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : ∀ (x : H × I), x ∈ mrange f ↔ x ∈ e₁.mgraph
e₂ : I →* H
he₂ : ∀ (x : I × H), x ∈ mrange (MulEquiv.prodComm.toMonoidHom.comp f) ↔ x ∈ e₂.mgraph
h : H
i : I
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
aesop (add simp [Prod.swap_eq_iff_eq_swap])

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₄
⊢ (f.prodMap g).range = f.range.prod g.range

Tactic:
ext ⟨_, _⟩

Goal state after:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₄
fst✝ : M₃
snd✝ : M₄
⊢ (fst✝, snd✝) ∈ (f.prodMap g).range ↔ (fst✝, snd✝) ∈ f.range.prod g.range
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_3
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
hb : ∀ i ∈ J, b i = 0
⊢ (if h : j ∈ I then proj ⟨j, h⟩ else 0) ((pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ⟨b, hb✝⟩) = b j

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∈ I
⊢ (proj ⟨j, h⟩) ((pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ⟨b, hb✝⟩) = b j

case neg
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∉ I
⊢ 0 ((pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ⟨b, hb✝⟩) = b j
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : (y, z) ∈ (f.coprod g).ker
⊢ (y, z) ∈ f.ker.prod g.ker

Tactic:
simp only [mem_ker, mem_prod, coprod_apply] at h ⊢

Goal state after:
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
⊢ f y = 0 ∧ g z = 0
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ ↑(Ioo (pred a) b) = ↑(Ico a b)

Tactic:
by simpa using Set.Ioo_pred_left_eq_Ioc_of_not_isMin ha _

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case intro
R : Type u
inst✝¹ : Semiring R
ι : Type v
inst✝ : Finite ι
motive : (N : Type u) → [inst : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
val✝ : Fintype ι
⊢ ∀ (M : ι → Type u) [inst : (i : ι) → AddCommMonoid (M i)] [inst_1 : (i : ι) → Module R (M i)],
    (∀ (i : ι), motive (M i)) → motive' ((i : ι) → M i)

Tactic:
refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι

Goal state after:
case intro
R : Type u
inst✝¹ : Semiring R
ι : Type v
inst✝ : Finite ι
motive : (N : Type u) → [inst : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
val✝ : Fintype ι
α : Type v
x✝² : Fintype α
h :
  ∀ (M : α → Type u) [inst : (i : α) → AddCommMonoid (M i)] [inst_1 : (i : α) → Module R (M i)],
    (∀ (i : α), motive (M i)) → motive' ((i : α) → M i)
M : Option α → Type u
x✝¹ : (i : Option α) → AddCommMonoid (M i)
x✝ : (i : Option α) → Module R (M i)
hn : ∀ (i : Option α), motive (M i)
⊢ motive' ((i : Option α) → M i)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case intro
ι : Type v
inst✝¹ : Finite ι
R : Type u_1
inst✝ : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
val✝ : Fintype ι
⊢ ∀ (M : ι → Type u) [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)],
    (∀ (i : ι), motive (M i)) → motive' ((i : ι) → M i)

Tactic:
refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι

Goal state after:
case intro
ι : Type v
inst✝¹ : Finite ι
R : Type u_1
inst✝ : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
val✝ : Fintype ι
α : Type v
x✝² : Fintype α
h :
  ∀ (M : α → Type u) [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)],
    (∀ (i : α), motive (M i)) → motive' ((i : α) → M i)
M : Option α → Type u
x✝¹ : (i : Option α) → AddCommGroup (M i)
x✝ : (i : Option α) → Module R (M i)
hn : ∀ (i : Option α), motive (M i)
⊢ motive' ((i : Option α) → M i)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
⊢ (disjointed f i ⊔ (Iio i).sup fun x ↦ disjointed f x) = (partialSups f) i

Tactic:
have hun : (Iio i).biUnion Iic = Iio i := by
      ext r; simpa using ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩

Goal state after:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ (disjointed f i ⊔ (Iio i).sup fun x ↦ disjointed f x) = (partialSups f) i
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ (disjointed f i ⊔ (Iio i).sup fun x ↦ disjointed f x) = (partialSups f) i

Tactic:
rw [← hun, sup_biUnion, sup_congr rfl (g := partialSups f)]

Goal state after:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ disjointed f i ⊔ (Iio i).sup ⇑(partialSups f) = (partialSups f) i

case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ ∀ a ∈ Iio i, ((Iic a).sup fun x ↦ disjointed f x) = (partialSups f) a