harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/ContextFreeGrammar.lean
/-- Add extra postfix to context-free rewriting. -/
lemma Rewrites.append_right (hvw : r.Rewrites u v) (p : List (Symbol T N)) :
    r.Rewrites (u ++ p) (v ++ p)

Proof state:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : r.Rewrites u v
p : List (Symbol T N)
⊢ r.Rewrites (u ++ p) (v ++ p)

Tactic:
rw [rewrites_iff] at *

Result:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : ∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
p : List (Symbol T N)
⊢ ∃ p_1 q, u ++ p = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ v ++ p = p_1 ++ r.output ++ q

Proof state:
case intro.intro
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ ∃ p_1 q, u ++ p = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ v ++ p = p_1 ++ r.output ++ q

Tactic:
use x, y ++ p

Result:
case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ u ++ p = x ++ [Symbol.nonterminal r.input] ++ (y ++ p) ∧ v ++ p = x ++ r.output ++ (y ++ p)

Proof state:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : ∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
p : List (Symbol T N)
⊢ ∃ p_1 q, u ++ p = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ v ++ p = p_1 ++ r.output ++ q

Tactic:
rcases hvw with ⟨x, y, hxy⟩

Result:
case intro.intro
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ ∃ p_1 q, u ++ p = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ v ++ p = p_1 ++ r.output ++ q

Proof state:
case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ u ++ p = x ++ [Symbol.nonterminal r.input] ++ (y ++ p) ∧ v ++ p = x ++ r.output ++ (y ++ p)

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem length_erase_of_mem [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) :
    length (l.erase a) = length l - 1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ (l.erase a).length = l.length - 1

Tactic:
rw [erase_eq_eraseP]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ (eraseP (fun x => a == x) l).length = l.length - 1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ (eraseP (fun x => a == x) l).length = l.length - 1

Tactic:
exact length_eraseP_of_mem h (beq_self_eq_true a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_eq_map (p : α → Prop) (f : α → β) (l : Array α) (H) :
    @pmap _ _ p (fun a _ => f a) l H = map f l

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : α → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ pmap (fun a x => f a) { toList := toList✝ } H = map f { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : α → β
l : Array α
H : ∀ (a : α), a ∈ l → p a
⊢ pmap (fun a x => f a) l H = map f l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : α → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ pmap (fun a x => f a) { toList := toList✝ } H = map f { toList := toList✝ }
-- Mathlib/Algebra/BigOperators/Associated.lean
theorem prod_mk {p : Multiset α} : (p.map Associates.mk).prod = Associates.mk p.prod :=
  Multiset.induction_on p (by simp) fun a s ih => by simp [ih, Associates.mk_mul_mk]

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p : Multiset α
⊢ (Multiset.map Associates.mk 0).prod = Associates.mk (Multiset.prod 0)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p : Multiset α
a : α
s : Multiset α
ih : (Multiset.map Associates.mk s).prod = Associates.mk s.prod
⊢ (Multiset.map Associates.mk (a ::ₘ s)).prod = Associates.mk (a ::ₘ s).prod

Tactic:
simp [ih, Associates.mk_mul_mk]

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem exists_countable_dense_no_bot_top [SeparableSpace α] [Nontrivial α] :
    ∃ s : Set α, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∉ s) ∧ ∀ x, IsTop x → x ∉ s

Proof state:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : SeparableSpace α
inst✝ : Nontrivial α
⊢ ∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∉ s) ∧ ∀ (x : α), IsTop x → x ∉ s

Tactic:
simpa using dense_univ.exists_countable_dense_subset_no_bot_top

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem isCyclic_of_prime_card {p : ℕ} [hp : Fact p.Prime]
    (h : Nat.card α = p) : IsCyclic α

Proof state:
case intro
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
this✝ : Finite α
this : Nontrivial α
g : α
hg : g ≠ 1
⊢ IsCyclic α

Tactic:
exact ⟨g, fun g' ↦ mem_zpowers_of_prime_card h hg⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
⊢ IsCyclic α

Tactic:
have : Finite α := Nat.finite_of_card_ne_zero (h ▸ hp.1.ne_zero)

Result:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
this : Finite α
⊢ IsCyclic α

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
this : Finite α
⊢ IsCyclic α

Tactic:
have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp (h ▸ hp.1.one_lt)

Result:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
this✝ : Finite α
this : Nontrivial α
⊢ IsCyclic α

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
this✝ : Finite α
this : Nontrivial α
⊢ IsCyclic α

Tactic:
obtain ⟨g, hg⟩ : ∃ g : α, g ≠ 1 := exists_ne 1

Result:
case intro
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
this✝ : Finite α
this : Nontrivial α
g : α
hg : g ≠ 1
⊢ IsCyclic α
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem aemeasurable_coe_nnreal_real_iff {f : α → ℝ≥0} {μ : Measure α} :
    AEMeasurable (fun x => f x : α → ℝ) μ ↔ AEMeasurable f μ :=
  ⟨fun h ↦ by simpa only [Real.toNNReal_coe] using h.real_toNNReal, AEMeasurable.coe_nnreal_real⟩

Proof state:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
μ : Measure α
h : AEMeasurable (fun x => ↑(f x)) μ
⊢ AEMeasurable f μ

Tactic:
simpa only [Real.toNNReal_coe] using h.real_toNNReal

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma eval₂_minpolyDiv_of_eval₂_eq_zero {T} [CommRing T]
    [IsDomain T] [DecidableEq T] {x y}
    (σ : S →+* T) (hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0) :
    eval₂ σ y (minpolyDiv R x) =
      if σ x = y then σ (aeval x (derivative <| minpoly R x)) else 0

Proof state:
case neg
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ σ y (minpolyDiv R x * (X - C x)) = 0
h : ¬σ x = y
⊢ eval₂ σ y (minpolyDiv R x) = 0

Tactic:
simpa [sub_eq_zero, Ne.symm h] using hy

Result:
no goals

Proof state:
case neg
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : ¬σ x = y
⊢ eval₂ σ y (minpolyDiv R x) = 0

Tactic:
rw [← eval₂_map, ← minpolyDiv_spec] at hy

Result:
case neg
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ σ y (minpolyDiv R x * (X - C x)) = 0
h : ¬σ x = y
⊢ eval₂ σ y (minpolyDiv R x) = 0

Proof state:
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
⊢ eval₂ σ y (minpolyDiv R x) = if σ x = y then σ ((aeval x) (derivative (minpoly R x))) else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : σ x = y
⊢ eval₂ σ y (minpolyDiv R x) = σ ((aeval x) (derivative (minpoly R x)))

case neg
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : ¬σ x = y
⊢ eval₂ σ y (minpolyDiv R x) = 0

Proof state:
case pos
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : σ x = y
⊢ eval₂ σ y (minpolyDiv R x) = σ ((aeval x) (derivative (minpoly R x)))

Tactic:
rw [← h, eval₂_hom, eval_minpolyDiv_self]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
theorem pi_map_π_apply' {β : Type v} {f g : β → Type v} (α : ∀ j, f j ⟶ g j) (b : β) (x) :
    (Pi.π g b : ∏ᶜ g → g b) (Pi.map α x) = α b ((Pi.π f b : ∏ᶜ f → f b) x)

Proof state:
β : Type v
f g : β → Type v
α : (j : β) → f j ⟶ g j
b : β
x : ∏ᶜ f
⊢ Pi.π g b (Pi.map α x) = α b (Pi.π f b x)

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Integral.lean
theorem setIntegral_restrict (hs : MeasurableSet s) (t : Set β) :
    ∫ x in t, f x ∂κ.restrict hs a = ∫ x in t ∩ s, f x ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
s : Set β
hs : MeasurableSet s
t : Set β
⊢ ∫ (x : β) in t, f x ∂(κ.restrict hs) a = ∫ (x : β) in t ∩ s, f x ∂κ a

Tactic:
rw [restrict_apply, Measure.restrict_restrict' hs]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem areaForm_neg_orientation : (-o).areaForm = -o.areaForm

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ (-o).areaForm = -o.areaForm

Tactic:
ext x y

Result:
case h.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ((-o).areaForm x) y = ((-o.areaForm) x) y

Proof state:
case h.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ((-o).areaForm x) y = ((-o.areaForm) x) y

Tactic:
simp [areaForm_to_volumeForm]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem pmap_map {p : β → Prop} (f₁ : (b : β) → p b → γ) (f₂ : α → β)
    (H : ∀ x ∈ (xs.map f₂).toList, p x):
    pmap f₁ (map f₂ xs) H = pmap (fun x hx => f₁ (f₂ x) hx) xs (by simpa using H)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ : Type u_5
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s : σ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
f₁✝ : β → σ₁ → σ₁ × γ
f₂✝ : α → σ₂ → σ₂ × β
p : β → Prop
f₁ : (b : β) → p b → γ
f₂ : α → β
H : ∀ x ∈ (map f₂ xs).toList, p x
⊢ ∀ x ∈ xs.toList, p (f₂ x)

Tactic:
simpa using H

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : β → Prop
f₁ : (b : β) → p b → γ
f₂ : α → β
H : ∀ x ∈ (map f₂ xs).toList, p x
⊢ pmap f₁ (map f₂ xs) H = pmap (fun x hx => f₁ (f₂ x) hx) xs ⋯

Tactic:
induction xs <;> simp_all

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem fg_iff_exists_fin_generating_family {N : L.Substructure M} :
    N.FG ↔ ∃ (n : ℕ) (s : Fin n → M), closure L (range s) = N

Proof state:
case mp
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Finite ∧ (closure L).toFun S = N) → ∃ n s, (closure L).toFun (range s) = N

Tactic:
rintro ⟨S, Sfin, hS⟩

Result:
case mp.intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Sfin : S.Finite
hS : (closure L).toFun S = N
⊢ ∃ n s, (closure L).toFun (range s) = N

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Finite ∧ (closure L).toFun S = N) ↔ ∃ n s, (closure L).toFun (range s) = N

Tactic:
constructor

Result:
case mp
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Finite ∧ (closure L).toFun S = N) → ∃ n s, (closure L).toFun (range s) = N

case mpr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ n s, (closure L).toFun (range s) = N) → ∃ S, S.Finite ∧ (closure L).toFun S = N

Proof state:
case mp.intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Sfin : S.Finite
hS : (closure L).toFun S = N
⊢ ∃ n s, (closure L).toFun (range s) = N

Tactic:
obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding

Result:
case mp.intro.intro.intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
n : ℕ
f : Fin n ↪ M
Sfin : (range ⇑f).Finite
hS : (closure L).toFun (range ⇑f) = N
⊢ ∃ n s, (closure L).toFun (range s) = N

Proof state:
case mpr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ n s, (closure L).toFun (range s) = N) → ∃ S, S.Finite ∧ (closure L).toFun S = N

Tactic:
rintro ⟨n, s, hs⟩

Result:
case mpr.intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
n : ℕ
s : Fin n → M
hs : (closure L).toFun (range s) = N
⊢ ∃ S, S.Finite ∧ (closure L).toFun S = N

Proof state:
case mpr.intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
n : ℕ
s : Fin n → M
hs : (closure L).toFun (range s) = N
⊢ ∃ S, S.Finite ∧ (closure L).toFun S = N

Tactic:
exact ⟨range s, finite_range s, hs⟩

Result:
no goals

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ N.FG ↔ ∃ n s, (closure L).toFun (range s) = N

Tactic:
rw [fg_def]

Result:
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Finite ∧ (closure L).toFun S = N) ↔ ∃ n s, (closure L).toFun (range s) = N

Proof state:
case mp.intro.intro.intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
n : ℕ
f : Fin n ↪ M
Sfin : (range ⇑f).Finite
hS : (closure L).toFun (range ⇑f) = N
⊢ ∃ n s, (closure L).toFun (range s) = N

Tactic:
exact ⟨n, f, hS⟩

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Divisibility.lean
theorem isUnit_iff : IsUnit a ↔ a = 1

Proof state:
case inr.intro.ha
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ a

Tactic:
exact one_le_iff_ne_zero.mpr ha

Result:
no goals

Proof state:
case inr.intro
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : 1 = a * t
⊢ a = 1

Tactic:
rw [eq_comm, mul_eq_one_iff_of_one_le] at ht

Result:
case inr.intro
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a = 1 ∧ t = 1
⊢ a = 1

case inr.intro.ha
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ a

case inr.intro.hb
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ t

Proof state:
a : Cardinal.{u}
⊢ IsUnit a ↔ a = 1

Tactic:
refine
  ⟨fun h => ?_, by
    rintro rfl
    exact isUnit_one⟩

Result:
a : Cardinal.{u}
h : IsUnit a
⊢ a = 1

Proof state:
case inr
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
⊢ a = 1

Tactic:
obtain ⟨t, ht⟩ := h 1

Result:
case inr.intro
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : 1 = a * t
⊢ a = 1

Proof state:
case inl
h : IsUnit 0
⊢ 0 = 1

Tactic:
exact (not_isUnit_zero h).elim

Result:
no goals

Proof state:
case inr.intro.hb
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ t ≠ 0

Tactic:
intro h

Result:
case inr.intro.hb
a : Cardinal.{u}
h✝ : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
h : t = 0
⊢ False

Proof state:
a : Cardinal.{u}
⊢ a = 1 → IsUnit a

Tactic:
rintro rfl

Result:
⊢ IsUnit 1

Proof state:
a : Cardinal.{u}
h : IsUnit a
⊢ a = 1

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case inl
h : IsUnit 0
⊢ 0 = 1

case inr
a : Cardinal.{u}
h : IsUnit a
ha : a ≠ 0
⊢ a = 1

Proof state:
case inr.intro.hb
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ t

Tactic:
apply one_le_iff_ne_zero.mpr

Result:
case inr.intro.hb
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ t ≠ 0

Proof state:
⊢ IsUnit 1

Tactic:
exact isUnit_one

Result:
no goals

Proof state:
case inr
a : Cardinal.{u}
h : IsUnit a
ha : a ≠ 0
⊢ a = 1

Tactic:
rw [isUnit_iff_forall_dvd] at h

Result:
case inr
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
⊢ a = 1

Proof state:
case inr.intro.hb
a : Cardinal.{u}
h✝ : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
h : t = 0
⊢ False

Tactic:
rw [h, mul_zero] at ht

Result:
case inr.intro.hb
a : Cardinal.{u}
h✝ : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : 0 = 1
h : t = 0
⊢ False

Proof state:
case inr.intro
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a = 1 ∧ t = 1
⊢ a = 1

Tactic:
exact ht.1

Result:
no goals

Proof state:
case inr.intro.hb
a : Cardinal.{u}
h✝ : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : 0 = 1
h : t = 0
⊢ False

Tactic:
exact zero_ne_one ht

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem coe_real_preimage_closedBall_period_zero (x ε : ℝ) :
    (↑) ⁻¹' closedBall (x : AddCircle (0 : ℝ)) ε = closedBall x ε

Proof state:
case h
x ε y : ℝ
⊢ y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ closedBall x ε

Tactic:
simp only [Set.mem_preimage, dist_eq_norm, AddCircle.norm_eq_of_zero, iff_self,
  ← QuotientAddGroup.mk_sub, Metric.mem_closedBall, Real.norm_eq_abs]

Result:
no goals

Proof state:
x ε : ℝ
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = closedBall x ε

Tactic:
ext y

Result:
case h
x ε y : ℝ
⊢ y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ closedBall x ε
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem IsOrtho.map (f : E →ₗᵢ[𝕜] F) {U V : Submodule 𝕜 E} (h : U ⟂ V) : U.map f ⟂ V.map f

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : ∀ u ∈ U, ∀ v ∈ V, inner u v = 0
⊢ ∀ u ∈ Submodule.map f U, ∀ v ∈ Submodule.map f V, inner u v = 0

Tactic:
simp_rw [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
  LinearIsometry.inner_map_map]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : ∀ u ∈ U, ∀ v ∈ V, inner u v = 0
⊢ ∀ a ∈ U, ∀ a_2 ∈ V, inner a a_2 = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : ∀ u ∈ U, ∀ v ∈ V, inner u v = 0
⊢ ∀ a ∈ U, ∀ a_2 ∈ V, inner a a_2 = 0

Tactic:
exact h

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : U ⟂ V
⊢ Submodule.map f U ⟂ Submodule.map f V

Tactic:
rw [isOrtho_iff_inner_eq] at *

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : ∀ u ∈ U, ∀ v ∈ V, inner u v = 0
⊢ ∀ u ∈ Submodule.map f U, ∀ v ∈ Submodule.map f V, inner u v = 0
-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.of_hasBasis_nhds {s : Set (Set α)}
    (h_nhds : ∀ a, (𝓝 a).HasBasis (fun t ↦ t ∈ s ∧ a ∈ t) id) : IsTopologicalBasis s where
  exists_subset_inter t₁ ht₁ t₂ ht₂ x hx

Proof state:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_nhds : ∀ (a : α), (𝓝 a).HasBasis (fun t => t ∈ s ∧ a ∈ t) id
t₁ : Set α
ht₁ : t₁ ∈ s
t₂ : Set α
ht₂ : t₂ ∈ s
x : α
hx : x ∈ t₁ ∩ t₂
⊢ ∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
simpa only [and_assoc, (h_nhds x).mem_iff]
  using (inter_mem ((h_nhds _).mem_of_mem ⟨ht₁, hx.1⟩) ((h_nhds _).mem_of_mem ⟨ht₂, hx.2⟩))

Result:
no goals

Proof state:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_nhds : ∀ (a : α), (𝓝 a).HasBasis (fun t => t ∈ s ∧ a ∈ t) id
x : α
⊢ 𝓝 x = 𝓝 x

Tactic:
simpa only [nhds_generateFrom, and_comm] using (h_nhds x).eq_biInf

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
@[reassoc (attr := simp)]
lemma rightDerivedNatTrans_comp (τ : F ⟶ F') (τ' : F' ⟶ F'') :
    rightDerivedNatTrans RF RF' α α' W τ ≫ rightDerivedNatTrans RF' RF'' α' α'' W τ' =
    rightDerivedNatTrans RF RF'' α α'' W (τ ≫ τ') :=
  rightDerived_ext RF α W _ _ _ (by simp)

Proof state:
C : Type u_1
D : Type u_5
H : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_6, u_5} D
inst✝³ : Category.{u_2, u_3} H
RF RF' RF'' : D ⥤ H
F F' F'' : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
α'' : F'' ⟶ L ⋙ RF''
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : RF.IsRightDerivedFunctor α W
inst✝ : RF'.IsRightDerivedFunctor α' W
τ : F ⟶ F'
τ' : F' ⟶ F''
⊢ α ≫ whiskerLeft L (RF.rightDerivedNatTrans RF' α α' W τ ≫ RF'.rightDerivedNatTrans RF'' α' α'' W τ') =
    α ≫ whiskerLeft L (RF.rightDerivedNatTrans RF'' α α'' W (τ ≫ τ'))

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma mulOption_lt_iff_P1 {i j k l} :
    (⟦mulOption x y i k⟧ : Game) < -⟦mulOption x (-y) j l⟧ ↔
    P1 (x.moveLeft i) x (x.moveLeft j) y (y.moveLeft k) (-(-y).moveLeft l)

Proof state:
x y : PGame
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
⊢ ⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧ ↔ P1 (x.moveLeft i) x (x.moveLeft j) y (y.moveLeft k) (-(-y).moveLeft l)

Tactic:
dsimp only [P1, mulOption, quot_sub, quot_add]

Result:
x y : PGame
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
⊢ ⟦x.moveLeft i * y⟧ + ⟦x * y.moveLeft k⟧ - ⟦x.moveLeft i * y.moveLeft k⟧ <
      -(⟦x.moveLeft j * -y⟧ + ⟦x * (-y).moveLeft l⟧ - ⟦x.moveLeft j * (-y).moveLeft l⟧) ↔
    ⟦x.moveLeft i * y⟧ + ⟦x * y.moveLeft k⟧ - ⟦x.moveLeft i * y.moveLeft k⟧ <
      ⟦x.moveLeft j * y⟧ + ⟦x * -(-y).moveLeft l⟧ - ⟦x.moveLeft j * -(-y).moveLeft l⟧

Proof state:
x y : PGame
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
⊢ ⟦x.moveLeft i * y⟧ + ⟦x * y.moveLeft k⟧ - ⟦x.moveLeft i * y.moveLeft k⟧ <
      -(⟦x.moveLeft j * -y⟧ + ⟦x * (-y).moveLeft l⟧ - ⟦x.moveLeft j * (-y).moveLeft l⟧) ↔
    ⟦x.moveLeft i * y⟧ + ⟦x * y.moveLeft k⟧ - ⟦x.moveLeft i * y.moveLeft k⟧ <
      ⟦x.moveLeft j * y⟧ + ⟦x * -(-y).moveLeft l⟧ - ⟦x.moveLeft j * -(-y).moveLeft l⟧

Tactic:
simp_rw [neg_sub', neg_add, quot_mul_neg, neg_neg]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
@[simp] lemma valuation_mul (hx : x ≠ 0) (hy : y ≠ 0) :
    (x * y).valuation = x.valuation + y.valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(x * y).valuation = ↑x.valuation + ↑y.valuation

Tactic:
simp [← valuation_coe, Padic.valuation_mul (coe_ne_zero.2 hx) (coe_ne_zero.2 hy)]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).valuation = x.valuation + y.valuation

Tactic:
zify

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(x * y).valuation = ↑x.valuation + ↑y.valuation