mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ Ico (natAdd m i) (natAdd m j) ⊆ range (natAdd m)

Tactic:
exact Ico_subset_Ici_self.trans <| image_natAdd_Ici m i ▸ image_subset_range _ _

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
v : Basis ι R M
⊢ (ofEquivFun v.equivFun).repr = v.repr

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ #(if p 0 then Finset.cons 0 ({x ∈ map { toFun := succ, inj' := ⋯ } univ | p x}) ⋯
      else {x ∈ map { toFun := succ, inj' := ⋯ } univ | p x}) =
    if p 0 then #{x | p x.succ} + 1 else #{x | p x.succ}

Tactic:
apply_ite Finset.card,

Goal state after:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then #(Finset.cons 0 ({x ∈ map { toFun := succ, inj' := ⋯ } univ | p x}) ⋯)
    else #({x ∈ map { toFun := succ, inj' := ⋯ } univ | p x})) =
    if p 0 then #{x | p x.succ} + 1 else #{x | p x.succ}
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
x : Fin m ⊕ Fin n
⊢ (fun i ↦ Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) x) = x

Tactic:
by rcases x with y | y <;> simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(Ioc a b) = ↑b - ↑a

Tactic:
by rw [← Nat.card_Ioc, ← map_valEmbedding_Ioc, card_map]

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt1 h (vecCons x (vecCons y u)) = vecCons y (vecAlt1 ⋯ u)

Tactic:
by
  ext i
  simp_rw [vecAlt1]
  rcases i with ⟨⟨⟩ | i, hi⟩
  · rfl
  · simp [vecAlt1, Nat.add_right_comm, ← Nat.add_assoc]

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∉ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i

Tactic:
· rw [mem_mulSupport, not_not] at ha
      rw [ha, one_mul]
      apply Finset.prod_erase _ ha

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y✝ : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
h₂ : map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)
h₃ : ↑x ∈ map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩))
y : ↥(span R (range v))
hy₁ : y ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
hy₂ : (span R (range v)).subtype y = ↑x
h_x_eq_y : x = y
⊢ x ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)

Tactic:
h_x_eq_y

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y✝ : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
h₂ : map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)
h₃ : ↑x ∈ map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩))
y : ↥(span R (range v))
hy₁ : y ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
hy₂ : (span R (range v)).subtype y = ↑x
h_x_eq_y : x = y
⊢ y ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
i : ι
⊢ (Basis.singleton ι R).repr 1 = single i 1

Tactic:
by simp [Basis.singleton]

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

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
⊢ ¬LinearIndependent R v ↔ ∃ s f g, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i

Tactic:
by
  rw [linearIndependent_iff'ₛ]
  simp only [exists_prop, not_forall]

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inr.top
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
y_0 : ⊤ ≠ 0
⊢ x ^ (⊤ * z) = (x ^ ⊤) ^ z

pp: case inr.inr.inr.inr.coe
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
⊢ x ^ (↑a✝ * z) = (x ^ ↑a✝) ^ z

Tactic:
· rw [top_mul z_0, epow_top x_2, top_epow z_0]

Goal state after:
case inr.inr.inr.inr.coe
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
⊢ x ^ (↑a✝ * z) = (x ^ ↑a✝) ^ z
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

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
s : Finset ι
hv : ∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ↑↑s → R
hfg : ∑ i, f i • v ↑i = ∑ i, g i • v ↑i
i : ↑↑s
⊢ ∑ i ∈ s, (if hj : i ∈ s then f ⟨i, hj⟩ else 0) • v i = ∑ i ∈ s, (if hj : i ∈ s then g ⟨i, hj⟩ else 0) • v i

Tactic:
by simpa +contextual [← s.sum_attach]

Goal state after:
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 (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_le_castSucc, succAbove_of_le_castSucc, contractNth_apply_of_gt _ _ _ _ h,
        castSucc_succ] <;>
      simp only [le_def, val_succ, val_castSucc]

Goal state after:
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

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 + 1 ≤ ↑i
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case succ
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ (d + 1) ≡ b ^ (d + 1) [MOD n]

Tactic:
rw [Nat.pow_succ, Nat.pow_succ]
    exact hd.mul h

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

Goal state before:
pp: n a b m : ℕ
h : a ≡ b [MOD n]
⊢ a ^ m ≡ b ^ m [MOD n]

Tactic:
induction m with
  | zero => rfl
  | succ d hd =>
    rw [Nat.pow_succ, Nat.pow_succ]
    exact hd.mul h

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

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

Tactic:
by
  rw [add_comm, add_modEq_left_iff]

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

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ i < m ^ n, ∑ x, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑a / 1 % m * 1 + ∑ x, ↑a / m ^ (↑x + 1) % m * m ^ (↑x + 1) = ↑a

Tactic:
Nat.div_one,

Goal state after:
case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ i < m ^ n, ∑ x, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑a % m * 1 + ∑ x, ↑a / m ^ (↑x + 1) % m * m ^ (↑x + 1) = ↑a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ n = 0 → ¬m = 0

Tactic:
exact fun _ => hm

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

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ↑a / 1 % Fin.cons x xs 0 * 1 +
      ∑ x_1, (↑a / ∏ x_2, Fin.cons x xs (Fin.castLE ⋯ x_2)) % xs x_1 * ∏ x_2, Fin.cons x xs (Fin.castLE ⋯ x_2) =
    ↑a

Tactic:
Nat.div_one,

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ↑a % Fin.cons x xs 0 * 1 +
      ∑ x_1, (↑a / ∏ x_2, Fin.cons x xs (Fin.castLE ⋯ x_2)) % xs x_1 * ∏ x_2, Fin.cons x xs (Fin.castLE ⋯ x_2) =
    ↑a
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : InjOn f (f ⁻¹' s)
hsf : s ⊆ range f
⊢ Nat.card ↑(f ⁻¹' s) = Nat.card ↑s

Tactic:
← Nat.card_image_of_injOn hf,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : InjOn f (f ⁻¹' s)
hsf : s ⊆ range f
⊢ Nat.card ↑(f '' f ⁻¹' s) = Nat.card ↑s
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ lift.{v', v} (⨆ ι, #↑↑ι) ≤ lift.{v, v'} (⨆ ι, #↑↑ι)

Tactic:
lift_iSup bddAbove_of_small

Goal state after:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ ⨆ i, lift.{v', v} #↑↑i ≤ ⨆ i, lift.{v, v'} #↑↑i
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R' M₁
i : R' → R
j : M →+ M₁
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ Module.rank R M ≤ Module.rank R' M₁

Tactic:
by
  simpa only [lift_id] using lift_rank_le_of_injective_injectiveₛ i j hi hj hc

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

Goal state before:
pp: R₀ : Type u_1
S₀ : Type u_2
inst✝⁵ : CommSemiring R₀
inst✝⁴ : Semiring S₀
inst✝³ : Algebra R₀ S₀
R₁ : Type u_3
S₁ : Type u_4
inst✝² : CommSemiring R₁
inst✝¹ : Semiring S₁
inst✝ : Algebra R₁ S₁
i : R₀ ≃+* R₁
j : S₀ ≃+* S₁
hc : (algebraMap R₁ S₁).comp i.toRingHom = j.toRingHom.comp (algebraMap R₀ S₀)
⊢ finrank R₀ S₀ = finrank R₁ S₁

Tactic:
simpa using! (congr_arg Cardinal.toNat (lift_rank_eq_of_equiv_equiv i j hc))

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

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ lift.{v', v} (⨆ ι, #↑↑ι) ≤ lift.{v, v'} (⨆ ι, #↑↑ι)

Tactic:
lift_iSup bddAbove_of_small

Goal state after:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ ⨆ i, lift.{v', v} #↑↑i ≤ ⨆ i, lift.{v, v'} #↑↑i
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
hv : ∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
f : ↑↑s → R
hf₀ : ∑ i, f i • v ↑i = 0
i : ↑↑s
⊢ ∑ i ∈ s, (if hj : i ∈ s then f ⟨i, hj⟩ else 0) • v i = 0

Tactic:
by simpa +contextual [← s.sum_attach]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨x, y, z, w, hxy, hxz, hxw, hyz, hyw, hzw, hs⟩ ↦ ?_⟩
  · obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
    rw [← insert_eq_of_mem hx, ← insert_sdiff_singleton,
      encard_insert_of_notMem (fun h ↦ h.2 rfl), (by exact rfl : (4 : ℕ∞) = 3 + 1),
      (ENat.addLECancellable_of_ne_top ENat.one_ne_top).inj_left, encard_eq_three] at h
    obtain ⟨y, z, w, hyz, hyw, hzw, hs⟩ := h
    refine ⟨x, y, z, w, ?_, ?_, ?_, hyz, hyw, hzw, ?_⟩
    · rintro rfl; exact (hs.symm.subset (Or.inl rfl)).2 rfl
    · rintro rfl; exact (hs.symm.subset (Or.inr (Or.inl rfl))).2 rfl
    · rintro rfl; exact (hs.symm.subset (Or.inr (Or.inr rfl))).2 rfl
    rw [← hs, insert_sdiff_singleton, insert_eq_of_mem hx]
  rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_insert_of_notMem,
    encard_singleton] <;> grind

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

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
P : Submodule R M
b : Basis ι R ↥P
x : M
| x ∈ map P.subtype (span R (range ⇑b))

Tactic:
Submodule.map_span,

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M
b : Basis ι R ↥P
x : M
| x ∈ span R (⇑P.subtype '' range ⇑b)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Function.Bijective f
t : Set β
⊢ t ⊆ range f

Tactic:
simp [hf.surjective.range_eq]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (rightRel s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝

Tactic:
rw [rightRel_eq]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y ↦ y * x⁻¹ ∈ s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
⊢ (fst R B C).comp (f.prod g) = f

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
⊢ (snd R B C).comp (f.prod g) = g

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
h : G
hh : h ∈ ↑H
n : G
hn : n ∈ ↑N
hy : (fun x1 x2 ↦ x1 * x2) h n ∈ H ⊔ N
⊢ ∃ a, φ a = Quotient.mk'' ⟨(fun x1 x2 ↦ x1 * x2) h n, hy⟩

Tactic:
simp only [SetLike.mem_coe] at hn

Goal state after:
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
h : G
hh : h ∈ ↑H
n : G
hy : (fun x1 x2 ↦ x1 * x2) h n ∈ H ⊔ N
hn : n ∈ N
⊢ ∃ a, φ a = Quotient.mk'' ⟨(fun x1 x2 ↦ x1 * x2) h n, hy⟩
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 : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ y, f y = (a, b)) ↔ f' a = b
⊢ ∀ (x x_1 : G), f' ((Prod.fst ∘ ⇑f) x * (Prod.fst ∘ ⇑f) x_1) = f' ((Prod.fst ∘ ⇑f) x) * f' ((Prod.fst ∘ ⇑f) x_1)

Tactic:
rintro g₁ g₂

Goal state after:
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 : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ y, f y = (a, b)) ↔ f' a = b
g₁ g₂ : G
⊢ f' ((Prod.fst ∘ ⇑f) g₁ * (Prod.fst ∘ ⇑f) g₂) = f' ((Prod.fst ∘ ⇑f) g₁) * f' ((Prod.fst ∘ ⇑f) g₂)
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
⊢ p.liftQ f h ∘ₛₗ p.mkQ = f

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
⊢ (pi fun x ↦ 0) = 0

Tactic:
ext; rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
b x : α
⊢ x ∈ Icc (succ a) b ↔ x ∈ Ioc a b

Tactic:
mem_Icc,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
b x : α
⊢ succ a ≤ x ∧ x ≤ b ↔ x ∈ Ioc a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ a ≤ x ∧ x < succ b ↔ x ∈ Icc a b

Tactic:
mem_Icc,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ a ≤ x ∧ x < succ b ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: case succ.hg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p ≤ comap (f ^ k) p

Tactic:
exact p.le_comap_pow_of_le_comap h k

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a x : α
⊢ x ∈ Icc a (pred b) ↔ x ∈ Ico a b

Tactic:
mem_Icc,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a x : α
⊢ a ≤ x ∧ x ≤ pred b ↔ x ∈ Ico a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ pred a < x ∧ x ≤ b ↔ x ∈ Icc a b

Tactic:
mem_Icc,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ pred a < x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
| f x

Tactic:
pi_eq_sum_univ x,

Goal state after:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
| f (∑ i, x i • fun j ↦ if i = j then 1 else 0)
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 ι
α : 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)

Tactic:
exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)

Goal state after:
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 ι
α : 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)

Tactic:
exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ (⨆ i, f i) ⊔ a = ⨆ i, f i ⊔ a

Tactic:
refine le_antisymm (sup_le ?_ ?_) <| ciSup_le fun i ↦ sup_le_sup_right (le_ciSup f i) a
  · exact ciSup_le fun i ↦ le_ciSup_of_le i le_sup_left
  · exact le_ciSup_of_le (Classical.arbitrary ι) le_sup_right

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : IsGLB (Set.Ioi i) k
⊢ IsGLB (Set.Ioc i j) k

Tactic:
by
  simp_rw [IsGLB, IsGreatest, mem_upperBounds, mem_lowerBounds] at h ⊢
  refine ⟨fun x hx ↦ h.1 x hx.1, fun x hx ↦ h.2 x ?_⟩
  intro y hy
  rcases le_or_gt y j with h_le | h_lt
  · exact hx y ⟨hy, h_le⟩
  · exact le_trans (hx j ⟨hij_lt, le_rfl⟩) h_lt.le

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≤ 0

Tactic:
rw [toZ_of_lt hi]

Goal state after:
case refine_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ -↑(Nat.find ⋯) ≤ 0